let X be non empty directed Subset of [:S,T:]; :: according to WAYBEL_0:def 39 :: thesis: ex b₁ being Element of the carrier of [:S,T:] st
( X is_<=_than b₁ & ( for b₂ being Element of the carrier of [:S,T:] holds
( not X is_<=_than b₂ or b₁ <= b₂ ) ) )
reconsider X1 = proj1 X as non empty directed Subset of S by YELLOW_3:21, YELLOW_3:22;
reconsider X2 = proj2 X as non empty directed Subset of T by YELLOW_3:21, YELLOW_3:22;
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 b₁ being Element of the carrier of [:S,T:] holds
( not X is_<=_than b₁ or [x,y] <= b₁ ) ) )
thus [x,y] is_>=_than X by A1, A3, YELLOW_3:31; :: thesis: for b₁ being Element of the carrier of [:S,T:] holds
( not X is_<=_than b₁ or [x,y] <= b₁ )
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 A5, YELLOW_3:31;
then A7: y <= z `2 by A4;
z `1 is_>=_than X1 by A5, A6, YELLOW_3:31;
then x <= z `1 by A2;
hence [x,y] <= z by A6, A7, YELLOW_3:11; :: thesis: verum