let X be non empty Subset of [:S,T:]; :: according to WAYBEL_0:def 40 :: thesis: ex b₁ being M2(the carrier of [:S,T:]) st
( b₁ is_<=_than X & ( for b₂ being M2(the carrier of [:S,T:]) holds
( not b₂ is_<=_than X or b₂ <= b₁ ) ) )
not proj1 X is empty by YELLOW_3:21;
then consider s being Element of S such that
A1: s is_<=_than proj1 X and
A2: for y being Element of S st y is_<=_than proj1 X holds
s >= y by WAYBEL_0:def 40;
not proj2 X is empty by YELLOW_3:21;
then consider t being Element of T such that
A3: t is_<=_than proj2 X and
A4: for y being Element of T st y is_<=_than proj2 X holds
t >= y by WAYBEL_0:def 40;
take [s,t] ; :: thesis: ( [s,t] is_<=_than X & ( for b₁ being M2(the carrier of [:S,T:]) holds
( not b₁ is_<=_than X or b₁ <= [s,t] ) ) )
thus [s,t] is_<=_than X by A1, A3, YELLOW_3:34; :: thesis: for b₁ being M2(the carrier of [:S,T:]) holds
( not b₁ is_<=_than X or b₁ <= [s,t] )
let y be Element of [:S,T:]; :: thesis: ( not y is_<=_than X or y <= [s,t] )
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
then A5: y = [(y `1 ),(y `2 )] by MCART_1:23;
assume y is_<=_than X ; :: thesis: y <= [s,t]
then ( y `1 is_<=_than proj1 X & y `2 is_<=_than proj2 X ) by A5, YELLOW_3:34;
then ( s >= y `1 & t >= y `2 ) by A2, A4;
hence y <= [s,t] by A5, YELLOW_3:11; :: thesis: verum