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 X9 = 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 ;
set x = the Element of X9;
the Element of X9 in X ;
then reconsider x = the Element of X9 as Element of L ;
x is_>=_than {} ;
then A3: S₁[ {} ] ;

A4: now :: thesis: for x, B being set st x in Y & B c= Y & S₁[B] holds
S₁[B \/ {x}]

let x, B be set ; :: thesis: ( x in Y & B c= Y & S₁[B] implies S₁[B \/ {x}] )
assume that
A5: x in Y and
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 and
A7: y is_>=_than B ;
x in X by A5;
then reconsider x9 = x as Element of L ;
consider z being Element of L such that
A8: z in X and
A9: x9 <= z and
A10: y <= z by A1, A5, A6;
thus S₁[B \/ {x}] :: thesis: verum

proof

take z ; :: thesis: ( z in X & z is_>=_than B \/ {x} )
thus z in X by A8; :: 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 a9 = a as Element of L ;
assume a in B \/ {x} ; :: thesis: a <= z
then ( a9 in B or a9 in {x} ) by XBOOLE_0:def 3;
then ( y >= a9 or a9 = x ) by A7, TARSKI:def 1;
hence a <= z by A9, A10, ORDERS_2:3; :: thesis: verum

end;

end;

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

end;

assume A11: 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 ;
then ex x being Element of L st
( x in X & x is_>=_than {} ) by A11;
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 that
A12: x in X and
A13: y in X ; :: thesis: ex z being Element of L st
( z in X & x <= z & y <= z )
{x,y} c= X by A12, A13, ZFMISC_1:32;
then consider z being Element of L such that
A14: z in X and
A15: z is_>=_than {x,y} by A11;
take z ; :: thesis: ( z in X & x <= z & y <= z )
A16: x in {x,y} by TARSKI:def 2;
y in {x,y} by TARSKI:def 2;
hence ( z in X & x <= z & y <= z ) by A14, A15, A16; :: thesis: verum