let x be Element of [:S,T:]; :: according to WAYBEL_2:def 6 :: thesis: for b₁ being M3( bool the carrier of [:S,T:]) holds x "/\" ("\/" (b₁,[:S,T:])) = "\/" (({x} "/\" b₁),[:S,T:])
let D be non empty directed Subset of [:S,T:]; :: thesis: 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; :: thesis: verum