A1:
the carrier of T c= the carrier of T
;
consider t being Element of T such that
A2:
t is_<=_than the carrier of T
by YELLOW_0:def 4;
consider s being Element of S such that
A3:
s is_<=_than the carrier of S
by YELLOW_0:def 4;
take
[s,t]
; YELLOW_0:def 4 [s,t] is_<=_than the carrier of [:S,T:]
( the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] & the carrier of S c= the carrier of S )
by YELLOW_3:def 2;
hence
[s,t] is_<=_than the carrier of [:S,T:]
by A3, A2, A1, YELLOW_3:33; verum