let S, T be Semilattice; ( [: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)
; WAYBEL_2:def 6,WAYBEL_2:def 7 ( S is meet-continuous & T is meet-continuous )
hereby WAYBEL_2:def 6,
WAYBEL_2:def 7 T is meet-continuous
thus
S is
up-complete
by A1, WAYBEL_2:11;
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;
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;
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
;
verum
end;
thus
T is up-complete
by A1, WAYBEL_2:11; WAYBEL_2:def 7 T is satisfying_MC
set s = the Element of S;
let t be Element of T; WAYBEL_2:def 6 for b1 being M3( bool the carrier of T) holds t "/\" ("\/" (b1,T)) = "\/" (({t} "/\" b1),T)
let D be non empty directed Subset of T; 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
; verum