let L be up-complete LATTICE; :: thesis: ( L is meet-continuous iff ( SupMap L is meet-preserving & SupMap L is join-preserving ) )

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

hereby :: thesis: ( SupMap L is meet-preserving & SupMap L is join-preserving implies L is meet-continuous )

assume A2:
( SupMap L is meet-preserving & SupMap L is join-preserving )
; :: thesis: 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)

hence ( SupMap L is meet-preserving & SupMap L is join-preserving ) by Th39; :: thesis: verum

end;for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)

proof

then
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
;
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;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

hence ( SupMap L is meet-preserving & SupMap L is join-preserving ) by Th39; :: thesis: verum

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