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

( proj1 X is directed & not proj1 X is empty & Proj (f,("\/" ((proj2 X),S))) is directed-sups-preserving ) by A1, YELLOW_3:21, YELLOW_3:22;
then A3: Proj (f,("\/" ((proj2 X),S))) preserves_sup_of proj1 X ;
A4: ex_sup_of (Proj (f,(sup (proj2 X)))) .: (proj1 X),T by YELLOW_0:17;
assume A5: 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:])) )
then A6: ex_sup_of proj1 X,R by YELLOW_3:41;
A7: ex_sup_of proj2 X,S by A5, YELLOW_3:41;
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 object such that
A8: b1 in dom (Proj (f,(sup (proj2 X)))) and
A9: b1 in proj1 X and
A10: b = (Proj (f,(sup (proj2 X)))) . b1 by FUNCT_1:def 6;
reconsider b1 = b1 as Element of R by A8;
A11: (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 object such that
A12: k1 in dom (Proj (f,b1)) and
A13: k1 in proj2 X and
A14: k = (Proj (f,b1)) . k1 by FUNCT_1:def 6;
reconsider k1 = k1 as Element of S by A12;
k = f . (b1,k1) by A14, Th7;
hence k <= sup (f .: X) by A2, A9, A13, Th17, YELLOW_0:17; :: thesis: verum

end;

( not proj2 X is empty & proj2 X is directed & Proj (f,b1) is directed-sups-preserving ) by A1, YELLOW_3:21, YELLOW_3:22;
then A15: Proj (f,b1) preserves_sup_of proj2 X ;
A16: ex_sup_of (Proj (f,b1)) .: (proj2 X),T by YELLOW_0:17;
b = (Proj (f,b1)) . (sup (proj2 X)) by A10, Th9
.= sup ((Proj (f,b1)) .: (proj2 X)) by A7, A15 ;
hence b <= sup (f .: X) by A16, A11, YELLOW_0:def 9; :: thesis: verum

end;

then A17: (Proj (f,(sup (proj2 X)))) .: (proj1 X) is_<=_than sup (f .: X) ;
A18: sup (f .: X) <= f . (sup X) by A2, WAYBEL17:16;
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, A3 ;
then f . (sup X) <= sup (f .: X) by A17, A4, YELLOW_0:def 9;
hence ( ex_sup_of f .: X,T & "\/" ((f .: X),T) = f . ("\/" (X,[:R,S:])) ) by A18, 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 ; :: thesis: verum