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)
set t = the 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 = { the Element of T} as non empty directed Subset of T by WAYBEL_0:5;
reconsider ST = {[s, the Element of 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, the Element of T]} "/\" [:D,t9:]) = [(sup (proj1 ({[s, the Element of T]} "/\" [:D,t9:]))),(sup (proj2 ({[s, the Element of T]} "/\" [:D,t9:])))] by YELLOW_3:46;
thus sup ({s} "/\" D) = sup ((proj1 {[s, the Element of T]}) "/\" D) by FUNCT_5:12
.= sup ((proj1 {[s, the Element of T]}) "/\" (proj1 [:D,t9:])) by FUNCT_5:9
.= sup (proj1 ({[s, the Element of T]} "/\" [:D,t9:])) by Th24
.= (sup ({[s, the Element of T]} "/\" [:D,t9:])) `1 by A4
.= ([s, the Element of T] "/\" (sup [:D,t9:])) `1 by A2
.= ([s, the Element of T] `1) "/\" ((sup [:D,t9:]) `1) by Th13
.= s "/\" ((sup [:D,t9:]) `1)
.= s "/\" (sup (proj1 [:D,t9:])) by A3
.= s "/\" (sup D) by FUNCT_5:9 ; :: thesis: verum

end;

thus T is up-complete by A1, WAYBEL_2:11; :: according to WAYBEL_2:def 7 :: thesis: T is satisfying_MC
set s = the Element of S;
let t be Element of T; :: according to WAYBEL_2:def 6 :: thesis: for b₁ being M3( 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 = { the Element of 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 = {[ the Element of 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 ({[ the Element of S,t]} "/\" [:s9,D:]) = [(sup (proj1 ({[ the Element of S,t]} "/\" [:s9,D:]))),(sup (proj2 ({[ the Element of S,t]} "/\" [:s9,D:])))] by YELLOW_3:46;
thus sup ({t} "/\" D) = sup ((proj2 {[ the Element of S,t]}) "/\" D) by FUNCT_5:12
.= sup ((proj2 {[ the Element of S,t]}) "/\" (proj2 [:s9,D:])) by FUNCT_5:9
.= sup (proj2 ({[ the Element of S,t]} "/\" [:s9,D:])) by Th24
.= (sup ({[ the Element of S,t]} "/\" [:s9,D:])) `2 by A6
.= ([ the Element of S,t] "/\" (sup [:s9,D:])) `2 by A2
.= ([ the Element of S,t] `2) "/\" ((sup [:s9,D:]) `2) by Th13
.= t "/\" ((sup [:s9,D:]) `2)
.= t "/\" (sup (proj2 [:s9,D:])) by A5
.= t "/\" (sup D) by FUNCT_5:9 ; :: thesis: verum