let X be non empty directed Subset of [:S,T:]; :: according to WAYBEL_0:def 39 :: thesis: ex b_{1} being Element of the carrier of [:S,T:] st

( X is_<=_than b_{1} & ( for b_{2} being Element of the carrier of [:S,T:] holds

( not X is_<=_than b_{2} or b_{1} <= b_{2} ) ) )

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_{1} being Element of the carrier of [:S,T:] holds

( not X is_<=_than b_{1} or [x,y] <= b_{1} ) ) )

thus [x,y] is_>=_than X by A1, A3, YELLOW_3:31; :: thesis: for b_{1} being Element of the carrier of [:S,T:] holds

( not X is_<=_than b_{1} or [x,y] <= b_{1} )

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

( X is_<=_than b

( not X is_<=_than 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

( not X is_<=_than b

thus [x,y] is_>=_than X by A1, A3, YELLOW_3:31; :: thesis: for b

( not X is_<=_than 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