let S, T be Semilattice; :: thesis: ( [:S,T:] is meet-continuous implies ( S is meet-continuous & T is meet-continuous ) )
assume that
A1: [:S,T:] is up-complete and
A2: for x being Element of [:S,T:]
for D being non empty directed Subset of [:S,T:] holds x "/\" (sup D) = sup ({x} "/\" D) ; :: according to WAYBEL_2:def 6,WAYBEL_2:def 7 :: thesis: ( S is meet-continuous & T is meet-continuous )

hereby :: according to WAYBEL_2:def 6,WAYBEL_2:def 7 :: thesis: T is meet-continuous

thus S is up-complete by A1, WAYBEL_2:11; :: thesis: for s being Element of S
for D being non empty directed Subset of S holds sup ({s} "/\" D) = s "/\" (sup D)
consider t being Element of T;
let s be Element of S; :: thesis: for D being non empty directed Subset of S holds sup ({s} "/\" D) = s "/\" (sup D)
let D be non empty directed Subset of S; :: thesis: sup ({s} "/\" D) = s "/\" (sup D)
reconsider t9 = {t} as non empty directed Subset of T by WAYBEL_0:5;
reconsider ST = {[s,t]} as non empty directed Subset of [:S,T:] by WAYBEL_0:5;
ex_sup_of [:D,t9:],[:S,T:] by A1, WAYBEL_0:75;
then A3: sup [:D,t9:] = [(sup (proj1 [:D,t9:])),(sup (proj2 [:D,t9:]))] by YELLOW_3:46;
ex_sup_of ST "/\" [:D,t9:],[:S,T:] by A1, WAYBEL_0:75;
then A4: sup ({[s,t]} "/\" [:D,t9:]) = [(sup (proj1 ({[s,t]} "/\" [:D,t9:]))),(sup (proj2 ({[s,t]} "/\" [:D,t9:])))] by YELLOW_3:46;
thus sup ({s} "/\" D) = sup ((proj1 {[s,t]}) "/\" D) by FUNCT_5:15
.= sup ((proj1 {[s,t]}) "/\" (proj1 [:D,t9:])) by FUNCT_5:11
.= sup (proj1 ({[s,t]} "/\" [:D,t9:])) by Th24
.= (sup ({[s,t]} "/\" [:D,t9:])) `1 by A4, MCART_1:7
.= ([s,t] "/\" (sup [:D,t9:])) `1 by A2
.= ([s,t] `1 ) "/\" ((sup [:D,t9:]) `1 ) by Th13
.= s "/\" ((sup [:D,t9:]) `1 ) by MCART_1:7
.= s "/\" (sup (proj1 [:D,t9:])) by A3, MCART_1:7
.= s "/\" (sup D) by FUNCT_5:11 ; :: thesis: verum

end;

thus T is up-complete by A1, WAYBEL_2:11; :: according to WAYBEL_2:def 7 :: thesis: T is satisfying_MC
consider s being Element of S;
let t be Element of T; :: according to WAYBEL_2:def 6 :: thesis: for b₁ being M2( bool the carrier of T) holds t "/\" ("\/" b₁,T) = "\/" ({t} "/\" b₁),T
let D be non empty directed Subset of T; :: thesis: t "/\" ("\/" D,T) = "\/" ({t} "/\" D),T
reconsider s9 = {s} as non empty directed Subset of S by WAYBEL_0:5;
ex_sup_of [:s9,D:],[:S,T:] by A1, WAYBEL_0:75;
then A5: sup [:s9,D:] = [(sup (proj1 [:s9,D:])),(sup (proj2 [:s9,D:]))] by YELLOW_3:46;
reconsider ST = {[s,t]} as non empty directed Subset of [:S,T:] by WAYBEL_0:5;
ex_sup_of ST "/\" [:s9,D:],[:S,T:] by A1, WAYBEL_0:75;
then A6: sup ({[s,t]} "/\" [:s9,D:]) = [(sup (proj1 ({[s,t]} "/\" [:s9,D:]))),(sup (proj2 ({[s,t]} "/\" [:s9,D:])))] by YELLOW_3:46;
thus sup ({t} "/\" D) = sup ((proj2 {[s,t]}) "/\" D) by FUNCT_5:15
.= sup ((proj2 {[s,t]}) "/\" (proj2 [:s9,D:])) by FUNCT_5:11
.= sup (proj2 ({[s,t]} "/\" [:s9,D:])) by Th24
.= (sup ({[s,t]} "/\" [:s9,D:])) `2 by A6, MCART_1:7
.= ([s,t] "/\" (sup [:s9,D:])) `2 by A2
.= ([s,t] `2 ) "/\" ((sup [:s9,D:]) `2 ) by Th13
.= t "/\" ((sup [:s9,D:]) `2 ) by MCART_1:7
.= t "/\" (sup (proj2 [:s9,D:])) by A5, MCART_1:7
.= t "/\" (sup D) by FUNCT_5:11 ; :: thesis: verum