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 ) )

( x in X & x is_<=_than Y ) ; :: thesis: ( not X is empty & X is filtered )

{} 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 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; :: thesis: verum

( ( 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 A11:
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_{1}[Y] )

then reconsider X9 = X as non empty set ;

assume A1: X is filtered ; :: thesis: for Y being finite Subset of X holds S_{1}[Y]

let Y be finite Subset of X; :: thesis: S_{1}[Y]

defpred S_{1}[ 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_{1}[ {} ]
;

_{1}[Y]
from FINSET_1:sch 2(A2, A3, A4); :: thesis: verum

end;then reconsider X9 = X as non empty set ;

assume A1: X is filtered ; :: thesis: for Y being finite Subset of X holds S

let Y be finite Subset of X; :: thesis: S

defpred S

( 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_{1}[B] holds

S_{1}[B \/ {x}]

thus
SS

let x, B be set ; :: thesis: ( x in Y & B c= Y & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

A5: x in Y and

B c= Y ; :: thesis: ( S_{1}[B] implies S_{1}[B \/ {x}] )

assume S_{1}[B]
; :: thesis: S_{1}[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_{1}[B \/ {x}]
:: thesis: verum

end;assume that

A5: x in Y and

B c= Y ; :: thesis: ( S

assume S

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

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, TARSKI:def 1;

hence z <= a by A9, A10, ORDERS_2:3; :: thesis: verum

end;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, TARSKI:def 1;

hence z <= a by A9, A10, ORDERS_2:3; :: thesis: verum

( x in X & x is_<=_than Y ) ; :: thesis: ( not X is empty & X is filtered )

{} 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 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; :: thesis: verum