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