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 Y' = {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 X' = X as non empty directed Subset of S ;
Proj f,a preserves_sup_of X

proof

A3: sup Y' = a by YELLOW_0:39;
A4: f preserves_sup_of [:Y',X':] by A1, WAYBEL_0:def 37;
A5: (Proj f,a) .: X = f .: [:Y',X':] by Th15;
A6: ex_sup_of Y',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 [:Y',X':],[:R,S:] by A6, YELLOW_3:39;
sup ((Proj f,a) .: X) = sup (f .: [:Y',X':]) by Th15
.= f . (sup [:Y',X':]) by A8, A4, WAYBEL_0:def 31
.= f . (sup Y'),(sup X') 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 Y' = {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 X' = X as non empty directed Subset of R ;
Proj f,b preserves_sup_of X

proof

A9: sup Y' = b by YELLOW_0:39;
A10: f preserves_sup_of [:X',Y':] by A1, WAYBEL_0:def 37;
A11: (Proj f,b) .: X = f .: [:X',Y':] by Th14;
A12: ex_sup_of Y',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 [:X',Y':],[:R,S:] by A12, YELLOW_3:39;
sup ((Proj f,b) .: X) = sup (f .: [:X',Y':]) by Th14
.= f . (sup [:X',Y':]) by A14, A10, WAYBEL_0:def 31
.= f . (sup X'),(sup Y') 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