let R, S, T be complete LATTICE; :: thesis: for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj f,a is directed-sups-preserving & Proj f,b is directed-sups-preserving ) ) holds
f is directed-sups-preserving
let f be Function of [:R,S:],T; :: thesis: ( ( for a being Element of R
for b being Element of S holds
( Proj f,a is directed-sups-preserving & Proj f,b is directed-sups-preserving ) ) implies f is directed-sups-preserving )
assume A1: for a being Element of R
for b being Element of S holds
( Proj f,a is directed-sups-preserving & Proj f,b is directed-sups-preserving ) ; :: thesis: f is directed-sups-preserving
for X being Subset of [:R,S:] st not X is empty & X is directed holds
f preserves_sup_of X

proof

let X be Subset of [:R,S:]; :: thesis: ( not X is empty & X is directed implies f preserves_sup_of X )
assume ( not X is empty & X is directed ) ; :: thesis: f preserves_sup_of X
then reconsider X = X as non empty directed Subset of [:R,S:] ;
for a being Element of R
for b being Element of S holds
( Proj f,a is monotone & Proj f,b is monotone ) by A1, WAYBEL17:3;
then A2: f is monotone by Th12;
f preserves_sup_of X

proof

assume A3: ex_sup_of X,[:R,S:] ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: X,T & "\/" (f .: X),T = f . ("\/" X,[:R,S:]) )
A4: ex_sup_of f .: X,T by YELLOW_0:17;
A5: ( proj1 X is directed & not proj1 X is empty ) by YELLOW_3:21, YELLOW_3:22;
A6: ex_sup_of proj1 X,R by A3, YELLOW_3:41;
A7: ex_sup_of proj2 X,S by A3, YELLOW_3:41;
Proj f,("\/" (proj2 X),S) is directed-sups-preserving by A1;
then A8: Proj f,("\/" (proj2 X),S) preserves_sup_of proj1 X by A5, WAYBEL_0:def 37;
A9: f . (sup X) = f . (sup (proj1 X)),(sup (proj2 X)) by YELLOW_3:46
.= (Proj f,(sup (proj2 X))) . (sup (proj1 X)) by Th8
.= sup ((Proj f,(sup (proj2 X))) .: (proj1 X)) by A6, A8, WAYBEL_0:def 31 ;
for b being Element of T st b in (Proj f,(sup (proj2 X))) .: (proj1 X) holds
b <= sup (f .: X)

proof

let b be Element of T; :: thesis: ( b in (Proj f,(sup (proj2 X))) .: (proj1 X) implies b <= sup (f .: X) )
assume b in (Proj f,(sup (proj2 X))) .: (proj1 X) ; :: thesis: b <= sup (f .: X)
then consider b1 being set such that
A10: ( b1 in dom (Proj f,(sup (proj2 X))) & b1 in proj1 X & b = (Proj f,(sup (proj2 X))) . b1 ) by FUNCT_1:def 12;
reconsider b1 = b1 as Element of R by A10;
A11: ( not proj2 X is empty & proj2 X is directed ) by YELLOW_3:21, YELLOW_3:22;
Proj f,b1 is directed-sups-preserving by A1;
then A12: Proj f,b1 preserves_sup_of proj2 X by A11, WAYBEL_0:def 37;
A13: b = (Proj f,b1) . (sup (proj2 X)) by A10, Th9
.= sup ((Proj f,b1) .: (proj2 X)) by A7, A12, WAYBEL_0:def 31 ;
b <= sup (f .: X)

proof

A14: ex_sup_of (Proj f,b1) .: (proj2 X),T by YELLOW_0:17;
(Proj f,b1) .: (proj2 X) is_<=_than sup (f .: X)

proof

let k be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not k in (Proj f,b1) .: (proj2 X) or k <= sup (f .: X) )
assume k in (Proj f,b1) .: (proj2 X) ; :: thesis: k <= sup (f .: X)
then consider k1 being set such that
A15: ( k1 in dom (Proj f,b1) & k1 in proj2 X & k = (Proj f,b1) . k1 ) by FUNCT_1:def 12;
reconsider k1 = k1 as Element of S by A15;
k = f . b1,k1 by A15, Th7;
hence k <= sup (f .: X) by A2, A4, A10, A15, Th17; :: thesis: verum

end;

hence b <= sup (f .: X) by A13, A14, YELLOW_0:def 9; :: thesis: verum

end;

hence b <= sup (f .: X) ; :: thesis: verum

end;

then A16: (Proj f,(sup (proj2 X))) .: (proj1 X) is_<=_than sup (f .: X) by LATTICE3:def 9;
ex_sup_of (Proj f,(sup (proj2 X))) .: (proj1 X),T by YELLOW_0:17;
then A17: f . (sup X) <= sup (f .: X) by A9, A16, YELLOW_0:def 9;
sup (f .: X) <= f . (sup X) by A2, WAYBEL17:16;
hence ( ex_sup_of f .: X,T & "\/" (f .: X),T = f . ("\/" X,[:R,S:]) ) by A17, YELLOW_0:17, YELLOW_0:def 3; :: thesis: verum

end;

hence f preserves_sup_of X ; :: thesis: verum

end;

hence f is directed-sups-preserving by WAYBEL_0:def 37; :: thesis: verum