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

proof

reconsider Y9 = {a} as non empty directed Subset of R by WAYBEL_0:5;
let X be Subset of S; :: thesis: ( not X is empty & X is directed implies Proj (f,a) preserves_sup_of X )
assume ( not X is empty & X is directed ) ; :: thesis: Proj (f,a) preserves_sup_of X
then reconsider X9 = X as non empty directed Subset of S ;
Proj (f,a) preserves_sup_of X

proof

A3: sup Y9 = a by YELLOW_0:39;
A4: f preserves_sup_of [:Y9,X9:] by A1, WAYBEL_0:def 37;
A5: (Proj (f,a)) .: X = f .: [:Y9,X9:] by Th15;
A6: ex_sup_of Y9,R by YELLOW_0:38;
assume A7: ex_sup_of X,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (Proj (f,a)) .: X,T & "\/" (((Proj (f,a)) .: X),T) = (Proj (f,a)) . ("\/" (X,S)) )
then A8: ex_sup_of [:Y9,X9:],[:R,S:] by A6, YELLOW_3:39;
sup ((Proj (f,a)) .: X) = sup (f .: [:Y9,X9:]) by Th15
.= f . (sup [:Y9,X9:]) by A8, A4, WAYBEL_0:def 31
.= f . ((sup Y9),(sup X9)) by A7, A6, YELLOW_3:43
.= (Proj (f,a)) . (sup X) by A3, Th7 ;
hence ( ex_sup_of (Proj (f,a)) .: X,T & "\/" (((Proj (f,a)) .: X),T) = (Proj (f,a)) . ("\/" (X,S)) ) by A8, A4, A5, WAYBEL_0:def 31; :: thesis: verum

end;

hence Proj (f,a) preserves_sup_of X ; :: thesis: verum

end;

for X being Subset of R st not X is empty & X is directed holds
Proj (f,b) preserves_sup_of X

proof

reconsider Y9 = {b} as non empty directed Subset of S by WAYBEL_0:5;
let X be Subset of R; :: thesis: ( not X is empty & X is directed implies Proj (f,b) preserves_sup_of X )
assume ( not X is empty & X is directed ) ; :: thesis: Proj (f,b) preserves_sup_of X
then reconsider X9 = X as non empty directed Subset of R ;
Proj (f,b) preserves_sup_of X

proof

A9: sup Y9 = b by YELLOW_0:39;
A10: f preserves_sup_of [:X9,Y9:] by A1, WAYBEL_0:def 37;
A11: (Proj (f,b)) .: X = f .: [:X9,Y9:] by Th14;
A12: ex_sup_of Y9,S by YELLOW_0:38;
assume A13: ex_sup_of X,R ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (Proj (f,b)) .: X,T & "\/" (((Proj (f,b)) .: X),T) = (Proj (f,b)) . ("\/" (X,R)) )
then A14: ex_sup_of [:X9,Y9:],[:R,S:] by A12, YELLOW_3:39;
sup ((Proj (f,b)) .: X) = sup (f .: [:X9,Y9:]) by Th14
.= f . (sup [:X9,Y9:]) by A14, A10, WAYBEL_0:def 31
.= f . ((sup X9),(sup Y9)) by A13, A12, YELLOW_3:43
.= (Proj (f,b)) . (sup X) by A9, Th8 ;
hence ( ex_sup_of (Proj (f,b)) .: X,T & "\/" (((Proj (f,b)) .: X),T) = (Proj (f,b)) . ("\/" (X,R)) ) by A14, A10, A11, WAYBEL_0:def 31; :: thesis: verum

end;

hence Proj (f,b) preserves_sup_of X ; :: thesis: verum

end;

hence ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) by A2, WAYBEL_0:def 37; :: thesis: verum