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] ; :: according to YELLOW_0:def 4 :: thesis: [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; :: thesis: verum