let L be non empty transitive RelStr ; :: thesis: for X being Subset of L holds
( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) )
let X be Subset of L; :: thesis: ( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) )

hereby :: thesis: ( ( for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) ) implies ( not X is empty & X is directed ) )

assume not X is empty ; :: thesis: ( X is directed implies for Y being finite Subset of X holds S₁[Y] )
then reconsider X' = X as non empty set ;
assume A1: X is directed ; :: thesis: for Y being finite Subset of X holds S₁[Y]
let Y be finite Subset of X; :: thesis: S₁[Y]
defpred S₁[ set ] means ex x being Element of L st
( x in X & x is_>=_than $1 );
A2: Y is finite ;
consider x being Element of X';
( x in X & X c= the carrier of L ) ;
then reconsider x = x as Element of L ;
x is_>=_than {} by YELLOW_0:6;
then A3: S₁[ {} ] ;

A4: now

let x, B be set ; :: thesis: ( x in Y & B c= Y & S₁[B] implies S₁[B \/ {x}] )
assume A5: ( x in Y & B c= Y ) ; :: thesis: ( S₁[B] implies S₁[B \/ {x}] )
assume S₁[B] ; :: thesis: S₁[B \/ {x}]
then consider y being Element of L such that
A6: ( y in X & y is_>=_than B ) ;
x in X by A5;
then reconsider x' = x as Element of L ;
consider z being Element of L such that
A7: ( z in X & x' <= z & y <= z ) by A1, A5, A6, Def1;
thus S₁[B \/ {x}] :: thesis: verum

proof

take z ; :: thesis: ( z in X & z is_>=_than B \/ {x} )
thus z in X by A7; :: thesis: z is_>=_than B \/ {x}
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in B \/ {x} or a <= z )
reconsider a' = a as Element of L ;
assume a in B \/ {x} ; :: thesis: a <= z
then ( a' in B or a' in {x} ) by XBOOLE_0:def 3;
then ( y >= a' or a' = x ) by A6, LATTICE3:def 9, TARSKI:def 1;
hence a <= z by A7, ORDERS_2:26; :: thesis: verum

end;

end;

thus S₁[Y] from FINSET_1:sch 2(A2, A3, A4); :: thesis: verum

end;

assume A8: for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) ; :: thesis: ( not X is empty & X is directed )
{} c= X by XBOOLE_1:2;
then ex x being Element of L st
( x in X & x is_>=_than {} ) by A8;
hence not X is empty ; :: thesis: X is directed
let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & x <= z & y <= z ) )
assume ( x in X & y in X ) ; :: thesis: ex z being Element of L st
( z in X & x <= z & y <= z )
then {x,y} c= X by ZFMISC_1:38;
then consider z being Element of L such that
A9: ( z in X & z is_>=_than {x,y} ) by A8;
take z ; :: thesis: ( z in X & x <= z & y <= z )
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
hence ( z in X & x <= z & y <= z ) by A9, LATTICE3:def 9; :: thesis: verum