let S, T be sup-Semilattice; :: thesis: for f being Function of S,T holds
( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )

let f be Function of S,T; :: thesis: ( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )
A1: dom f = the carrier of S by FUNCT_2:def 1;
thus ( f is join-preserving implies for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) :: thesis: ( ( for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) implies f is join-preserving )
proof
assume A2: f is join-preserving ; :: thesis: for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y)
let z, y be Element of S; :: thesis: f . (z "\/" y) = (f . z) "\/" (f . y)
A3: f preserves_sup_of {z,y} by A2;
A4: ( f .: {z,y} = {(f . z),(f . y)} & ex_sup_of {z,y},S ) by ;
thus f . (z "\/" y) = f . (sup {z,y}) by YELLOW_0:41
.= sup {(f . z),(f . y)} by A4, A3
.= (f . z) "\/" (f . y) by YELLOW_0:41 ; :: thesis: verum
end;
assume A5: for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ; :: thesis:
for z, y being Element of S holds f preserves_sup_of {z,y}
proof
let z, y be Element of S; :: thesis:
A6: f .: {z,y} = {(f . z),(f . y)} by ;
then A7: ( ex_sup_of {z,y},S implies ex_sup_of f .: {z,y},T ) by YELLOW_0:20;
sup (f .: {z,y}) = (f . z) "\/" (f . y) by
.= f . (z "\/" y) by A5
.= f . (sup {z,y}) by YELLOW_0:41 ;
hence f preserves_sup_of {z,y} by A7; :: thesis: verum
end;
hence f is join-preserving ; :: thesis: verum