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 5;
consider s being Element of S such that
A3: s is_>=_than the carrier of S by YELLOW_0:def 5;
take [s,t] ; :: according to YELLOW_0:def 5 :: thesis: the carrier of [:S,T:] is_<=_than [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 the carrier of [:S,T:] is_<=_than [s,t] by A3, A2, A1, YELLOW_3:30; :: thesis: verum