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 R st not X is empty & X is directed holds
Proj f,b preserves_sup_of X

proof

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 ;
reconsider Y' = {b} as non empty directed Subset of S by WAYBEL_0:5;
Proj f,b preserves_sup_of X

proof

assume A3: 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) )
A4: ex_sup_of Y',S by YELLOW_0:38;
then A5: ex_sup_of [:X',Y':],[:R,S:] by A3, YELLOW_3:39;
A6: f preserves_sup_of [:X',Y':] by A1, WAYBEL_0:def 37;
A7: (Proj f,b) .: X = f .: [:X',Y':] by Th14;
A8: sup Y' = b by YELLOW_0:39;
sup ((Proj f,b) .: X) = sup (f .: [:X',Y':]) by Th14
.= f . (sup [:X',Y':]) by A5, A6, WAYBEL_0:def 31
.= f . (sup X'),(sup Y') by A3, A4, YELLOW_3:43
.= (Proj f,b) . (sup X) by A8, Th8 ;
hence ( ex_sup_of (Proj f,b) .: X,T & "\/" ((Proj f,b) .: X),T = (Proj f,b) . ("\/" X,R) ) by A5, A6, A7, WAYBEL_0:def 31; :: thesis: verum

end;

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

end;

for X being Subset of S st not X is empty & X is directed holds
Proj f,a preserves_sup_of X

proof

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 ;
reconsider Y' = {a} as non empty directed Subset of R by WAYBEL_0:5;
Proj f,a preserves_sup_of X

proof

assume A9: 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) )
A10: ex_sup_of Y',R by YELLOW_0:38;
then A11: ex_sup_of [:Y',X':],[:R,S:] by A9, YELLOW_3:39;
A12: f preserves_sup_of [:Y',X':] by A1, WAYBEL_0:def 37;
A13: (Proj f,a) .: X = f .: [:Y',X':] by Th15;
A14: sup Y' = a by YELLOW_0:39;
sup ((Proj f,a) .: X) = sup (f .: [:Y',X':]) by Th15
.= f . (sup [:Y',X':]) by A11, A12, WAYBEL_0:def 31
.= f . (sup Y'),(sup X') by A9, A10, YELLOW_3:43
.= (Proj f,a) . (sup X) by A14, Th7 ;
hence ( ex_sup_of (Proj f,a) .: X,T & "\/" ((Proj f,a) .: X),T = (Proj f,a) . ("\/" X,S) ) by A11, A12, A13, WAYBEL_0:def 31; :: thesis: verum

end;

hence Proj f,a 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