let X be non empty directed Subset of L2; :: thesis: ex x being Element of L2 st
( x is_>=_than X & ( for y being Element of L2 st y is_>=_than X holds
x <= y ) )
reconsider X9 = X as Subset of L1 by A1;
reconsider X9 = X9 as non empty directed Subset of L1 by A1, WAYBEL_0:3;
consider x9 being Element of L1 such that
A3: x9 is_>=_than X9 and
A4: for y9 being Element of L1 st y9 is_>=_than X9 holds
x9 <= y9 by A2, WAYBEL_0:def 39;
reconsider x = x9 as Element of L2 by A1;
take x = x; :: thesis: ( x is_>=_than X & ( for y being Element of L2 st y is_>=_than X holds
x <= y ) )
thus x is_>=_than X by A1, A3, YELLOW_0:2; :: thesis: for y being Element of L2 st y is_>=_than X holds
x <= y
let y be Element of L2; :: thesis: ( y is_>=_than X implies x <= y )
assume A5: y is_>=_than X ; :: thesis: x <= y
reconsider y9 = y as Element of L1 by A1;
x9 <= y9 by A1, A4, A5, YELLOW_0:2;
hence x <= y by A1; :: thesis: verum