let x be Element of [:S,T:]; :: according to WAYBEL_2:def 6 :: thesis: for b₁ being M2( 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;
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:23;
reconsider x' = {x} as non empty directed Subset of [:S,T:] by WAYBEL_0:5;
( ex_sup_of x' "/\" D,[:S,T:] & ex_sup_of D,[:S,T:] ) by WAYBEL_0:75;
then A5: sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
ex_sup_of x' "/\" D,[:S,T:] by WAYBEL_0:75;
then A6: sup ({x} "/\" D) = [(sup (proj1 ({x} "/\" D))),(sup (proj2 ({x} "/\" D)))] by YELLOW_3:46;
A7: (x "/\" (sup D)) `1 = (x `1 ) "/\" ((sup D) `1 ) by Th13
.= (x `1 ) "/\" (sup (proj1 D)) by A5, MCART_1:7
.= sup ({(x `1 )} "/\" (proj1 D)) by A1, WAYBEL_2:def 6
.= sup ((proj1 {x}) "/\" (proj1 D)) by A4, FUNCT_5:15
.= sup (proj1 ({x} "/\" D)) by Th24
.= (sup ({x} "/\" D)) `1 by A6, MCART_1:7 ;
(x "/\" (sup D)) `2 = (x `2 ) "/\" ((sup D) `2 ) by Th13
.= (x `2 ) "/\" (sup (proj2 D)) by A5, MCART_1:7
.= sup ({(x `2 )} "/\" (proj2 D)) by A2, WAYBEL_2:def 6
.= sup ((proj2 {x}) "/\" (proj2 D)) by A4, FUNCT_5:15
.= sup (proj2 ({x} "/\" D)) by Th24
.= (sup ({x} "/\" D)) `2 by A6, MCART_1:7 ;
hence x "/\" (sup D) = sup ({x} "/\" D) by A3, A7, DOMAIN_1:12; :: thesis: verum