let x be Element of [:S,T:]; :: according to WAYBEL_3:def 5 :: thesis: x = "\/" ((waybelow x),[:S,T:])
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
ex_sup_of waybelow x,[:S,T:] by WAYBEL_0:75;
then A2: sup (waybelow x) = [(sup (proj1 (waybelow x))),(sup (proj2 (waybelow x)))] by YELLOW_3:46;
then A3: (sup (waybelow x)) `2 = sup (proj2 (waybelow x))
.= sup (waybelow (x `2)) by Th47
.= x `2 by WAYBEL_3:def 5 ;
(sup (waybelow x)) `1 = sup (proj1 (waybelow x)) by A2
.= sup (waybelow (x `1)) by Th46
.= x `1 by WAYBEL_3:def 5 ;
hence x = "\/" ((waybelow x),[:S,T:]) by A1, A3, DOMAIN_1:2; :: thesis: verum