let X be non empty directed Subset of [:S,T:]; :: according to WAYBEL_0:def 39 :: thesis: ex b1 being Element of the carrier of [:S,T:] st
( X is_<=_than b1 & ( for b2 being Element of the carrier of [:S,T:] holds
( not X is_<=_than b2 or b1 <= b2 ) ) )

reconsider X1 = proj1 X as non empty directed Subset of S by ;
reconsider X2 = proj2 X as non empty directed Subset of T by ;
consider x being Element of S such that
A1: x is_>=_than X1 and
A2: for z being Element of S st z is_>=_than X1 holds
x <= z by WAYBEL_0:def 39;
consider y being Element of T such that
A3: y is_>=_than X2 and
A4: for z being Element of T st z is_>=_than X2 holds
y <= z by WAYBEL_0:def 39;
take [x,y] ; :: thesis: ( X is_<=_than [x,y] & ( for b1 being Element of the carrier of [:S,T:] holds
( not X is_<=_than b1 or [x,y] <= b1 ) ) )

thus [x,y] is_>=_than X by ; :: thesis: for b1 being Element of the carrier of [:S,T:] holds
( not X is_<=_than b1 or [x,y] <= b1 )

let z be Element of [:S,T:]; :: thesis: ( not X is_<=_than z or [x,y] <= z )
assume A5: z is_>=_than X ; :: thesis: [x,y] <= z
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
then A6: z = [(z `1),(z `2)] by MCART_1:21;
then z `2 is_>=_than X2 by ;
then A7: y <= z `2 by A4;
z `1 is_>=_than X1 by ;
then x <= z `1 by A2;
hence [x,y] <= z by ; :: thesis: verum