let X be non empty Subset of [:S,T:]; :: according to WAYBEL_0:def 40 :: thesis: ex b₁ being M3( the carrier of [:S,T:]) st
( b₁ is_<=_than X & ( for b₂ being M3( 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 M3( 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 M3( 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:21;
assume A6: y is_<=_than X ; :: thesis: y <= [s,t]
then y `2 is_<=_than proj2 X by A5, YELLOW_3:34;
then A7: t >= y `2 by A4;
y `1 is_<=_than proj1 X by A5, A6, YELLOW_3:34;
then s >= y `1 by A2;
hence y <= [s,t] by A5, A7, YELLOW_3:11; :: thesis: verum