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)
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)
consider t being Element of T;
reconsider t' = {t} as non empty directed Subset of T by WAYBEL_0:5;
ex_sup_of [:D,t':],[:S,T:] by A1, WAYBEL_0:75;
then A3: sup [:D,t':] = [(sup (proj1 [:D,t':])),(sup (proj2 [:D,t':]))] by YELLOW_3:46;
reconsider ST = {[s,t]} as non empty directed Subset of [:S,T:] by WAYBEL_0:5;
ex_sup_of ST "/\" [:D,t':],[:S,T:] by A1, WAYBEL_0:75;
then A4: sup ({[s,t]} "/\" [:D,t':]) = [(sup (proj1 ({[s,t]} "/\" [:D,t':]))),(sup (proj2 ({[s,t]} "/\" [:D,t':])))] by YELLOW_3:46;
thus sup ({s} "/\" D) = sup ((proj1 {[s,t]}) "/\" D) by FUNCT_5:15
.= sup ((proj1 {[s,t]}) "/\" (proj1 [:D,t':])) by FUNCT_5:11
.= sup (proj1 ({[s,t]} "/\" [:D,t':])) by Th24
.= (sup ({[s,t]} "/\" [:D,t':])) `1 by A4, MCART_1:7
.= ([s,t] "/\" (sup [:D,t':])) `1 by A2
.= ([s,t] `1 ) "/\" ((sup [:D,t':]) `1 ) by Th13
.= s "/\" ((sup [:D,t':]) `1 ) by MCART_1:7
.= s "/\" (sup (proj1 [:D,t':])) 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
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
consider s being Element of S;
reconsider s' = {s} as non empty directed Subset of S by WAYBEL_0:5;
ex_sup_of [:s',D:],[:S,T:] by A1, WAYBEL_0:75;
then A5: sup [:s',D:] = [(sup (proj1 [:s',D:])),(sup (proj2 [:s',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 "/\" [:s',D:],[:S,T:] by A1, WAYBEL_0:75;
then A6: sup ({[s,t]} "/\" [:s',D:]) = [(sup (proj1 ({[s,t]} "/\" [:s',D:]))),(sup (proj2 ({[s,t]} "/\" [:s',D:])))] by YELLOW_3:46;
thus sup ({t} "/\" D) = sup ((proj2 {[s,t]}) "/\" D) by FUNCT_5:15
.= sup ((proj2 {[s,t]}) "/\" (proj2 [:s',D:])) by FUNCT_5:11
.= sup (proj2 ({[s,t]} "/\" [:s',D:])) by Th24
.= (sup ({[s,t]} "/\" [:s',D:])) `2 by A6, MCART_1:7
.= ([s,t] "/\" (sup [:s',D:])) `2 by A2
.= ([s,t] `2 ) "/\" ((sup [:s',D:]) `2 ) by Th13
.= t "/\" ((sup [:s',D:]) `2 ) by MCART_1:7
.= t "/\" (sup (proj2 [:s',D:])) by A5, MCART_1:7
.= t "/\" (sup D) by FUNCT_5:11 ; :: thesis: verum