thus id L is sups-preserving :: thesis: id L is infs-preserving

proof

let X be Subset of L; :: according to WAYBEL_0:def 33 :: thesis: id L preserves_sup_of X
assume A1: ex_sup_of X,L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (id L) .: X,L & "\/" ((id L) .: X),L = (id L) . ("\/" X,L) )
( (id L) . (sup X) = sup X & (id L) .: X = X ) by FUNCT_1:162, TMAP_1:91;
hence ( ex_sup_of (id L) .: X,L & sup ((id L) .: X) = (id L) . (sup X) ) by A1; :: thesis: verum

end;

let X be Subset of L; :: according to WAYBEL_0:def 32 :: thesis: id L preserves_inf_of X
assume A2: ex_inf_of X,L ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (id L) .: X,L & "/\" ((id L) .: X),L = (id L) . ("/\" X,L) )
( (id L) . (inf X) = inf X & (id L) .: X = X ) by FUNCT_1:162, TMAP_1:91;
hence ( ex_inf_of (id L) .: X,L & "/\" ((id L) .: X),L = (id L) . ("/\" X,L) ) by A2; :: thesis: verum