let x be Element of [:S,T:]; :: according to WAYBEL_8:def 3 :: thesis: x = "\/" ((compactbelow x),[:S,T:])
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
A2: sup (compactbelow x) = [(sup (proj1 (compactbelow x))),(sup (proj2 (compactbelow x)))] by YELLOW_3:46;
then A3: (sup (compactbelow x)) `2 = sup (proj2 (compactbelow x))
.= sup (compactbelow (x `2)) by Th53
.= x `2 by WAYBEL_8:def 3 ;
(sup (compactbelow x)) `1 = sup (proj1 (compactbelow x)) by A2
.= sup (compactbelow (x `1)) by Th52
.= x `1 by WAYBEL_8:def 3 ;
hence x = "\/" ((compactbelow x),[:S,T:]) by A1, A3, DOMAIN_1:2; :: thesis: verum