let x be Element of [:S,T:]; WAYBEL_2:def 6 for b1 being M3( bool the carrier of [:S,T:]) holds x "/\" ("\/" (b1,[:S,T:])) = "\/" (({x} "/\" b1),[:S,T:])
let D be non empty directed Subset of [:S,T:]; x "/\" ("\/" (D,[:S,T:])) = "\/" (({x} "/\" D),[:S,T:])
A1:
( not proj1 D is empty & proj1 D is directed )
by YELLOW_3:21, YELLOW_3:22;
reconsider x9 = {x} as non empty directed Subset of [:S,T:] by WAYBEL_0:5;
A2:
( not proj2 D is empty & proj2 D is directed )
by YELLOW_3:21, YELLOW_3:22;
A3:
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then A4:
x = [(x `1),(x `2)]
by MCART_1:21;
ex_sup_of x9 "/\" D,[:S,T:]
by WAYBEL_0:75;
then A5:
sup ({x} "/\" D) = [(sup (proj1 ({x} "/\" D))),(sup (proj2 ({x} "/\" D)))]
by YELLOW_3:46;
ex_sup_of D,[:S,T:]
by WAYBEL_0:75;
then A6:
sup D = [(sup (proj1 D)),(sup (proj2 D))]
by YELLOW_3:46;
A7: (x "/\" (sup D)) `2 =
(x `2) "/\" ((sup D) `2)
by Th13
.=
(x `2) "/\" (sup (proj2 D))
by A6
.=
sup ({(x `2)} "/\" (proj2 D))
by A2, WAYBEL_2:def 6
.=
sup ((proj2 {x}) "/\" (proj2 D))
by A4, FUNCT_5:12
.=
sup (proj2 ({x} "/\" D))
by Th24
.=
(sup ({x} "/\" D)) `2
by A5
;
(x "/\" (sup D)) `1 =
(x `1) "/\" ((sup D) `1)
by Th13
.=
(x `1) "/\" (sup (proj1 D))
by A6
.=
sup ({(x `1)} "/\" (proj1 D))
by A1, WAYBEL_2:def 6
.=
sup ((proj1 {x}) "/\" (proj1 D))
by A4, FUNCT_5:12
.=
sup (proj1 ({x} "/\" D))
by Th24
.=
(sup ({x} "/\" D)) `1
by A5
;
hence
x "/\" (sup D) = sup ({x} "/\" D)
by A3, A7, DOMAIN_1:2; verum