let L be non empty transitive RelStr ; :: thesis: for X being Subset of L holds
( ( not X is empty & X is filtered ) 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 filtered ) 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 filtered ) )

assume not X is empty ; :: thesis: ( X is filtered implies for Y being finite Subset of X holds S₁[Y] )
then reconsider X9 = X as non empty set ;
assume A1: X is filtered ; :: 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 {} 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 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, Def2;
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 8 :: thesis: ( not a in B \/ {x} or z <= a )
reconsider a9 = a as Element of L ;
assume a in B \/ {x} ; :: thesis: z <= a
then ( a9 in B or a9 in {x} ) by XBOOLE_0:def 3;
then ( y <= a9 or a9 = x ) by A7, LATTICE3:def 8, TARSKI:def 1;
hence z <= a 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 filtered )
{} c= X by XBOOLE_1:2;
then ex x being Element of L st
( x in X & x is_<=_than {} ) by A11;
hence not X is empty ; :: thesis: X is filtered
let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & z <= x & z <= y ) )
assume that
A12: x in X and
A13: y in X ; :: thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
{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 & z <= x & z <= y )
A16: x in {x,y} by TARSKI:def 2;
y in {x,y} by TARSKI:def 2;
hence ( z in X & z <= x & z <= y ) by A14, A15, A16, LATTICE3:def 8; :: thesis: verum