let x be Element of [:S,T:]; WAYBEL_8:def 3 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; verum