let L be up-complete LATTICE; :: thesis: ( L is meet-continuous iff ( SupMap L is meet-preserving & SupMap L is join-preserving ) )
hereby :: thesis: ( SupMap L is meet-preserving & SupMap L is join-preserving implies L is meet-continuous )
assume A1: L is meet-continuous ; :: thesis: ( SupMap L is meet-preserving & SupMap L is join-preserving )
for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
proof
let D1, D2 be non empty directed Subset of L; :: thesis: (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) by A1, Th45;
then inf_op L is directed-sups-preserving by Th46;
hence (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43; :: thesis: verum
end;
then for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ;
hence ( SupMap L is meet-preserving & SupMap L is join-preserving ) by Th39; :: thesis: verum
end;
assume A2: ( SupMap L is meet-preserving & SupMap L is join-preserving ) ; :: thesis: L is meet-continuous
thus L is up-complete ; :: according to WAYBEL_2:def 7 :: thesis: L is satisfying_MC
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) by A2, Th38;
then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40;
hence L is satisfying_MC by Th44; :: thesis: verum