let L be non empty transitive RelStr ; :: thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds

ex_inf_of Y,L ) & ( for x being Element of L st x in F holds

ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds

"/\" (Y,L) in F ) holds

F is filtered

let X, F be Subset of L; :: thesis: ( ( for Y being finite Subset of X st Y <> {} holds

ex_inf_of Y,L ) & ( for x being Element of L st x in F holds

ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds

"/\" (Y,L) in F ) implies F is filtered )

assume that

A1: for Y being finite Subset of X st Y <> {} holds

ex_inf_of Y,L and

A2: for x being Element of L st x in F holds

ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) ) and

A3: for Y being finite Subset of X st Y <> {} holds

"/\" (Y,L) in F ; :: thesis: F is filtered

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( x in F & y in F implies ex z being Element of L st

( z in F & z <= x & z <= y ) )

assume A4: x in F ; :: thesis: ( not y in F or ex z being Element of L st

( z in F & z <= x & z <= y ) )

then consider Y1 being finite Subset of X such that

A5: ex_inf_of Y1,L and

A6: x = "/\" (Y1,L) by A2;

assume y in F ; :: thesis: ex z being Element of L st

( z in F & z <= x & z <= y )

then consider Y2 being finite Subset of X such that

A7: ex_inf_of Y2,L and

A8: y = "/\" (Y2,L) by A2;

take z = "/\" ((Y1 \/ Y2),L); :: thesis: ( z in F & z <= x & z <= y )

A9: ( ( Y1 = {} & Y2 = {} & {} \/ {} = {} ) or Y1 \/ Y2 <> {} ) ;

hence z in F by A3, A4, A6; :: thesis: ( z <= x & z <= y )

ex_inf_of Y1 \/ Y2,L by A1, A5, A9;

hence ( z <= x & z <= y ) by A5, A6, A7, A8, XBOOLE_1:7, YELLOW_0:35; :: thesis: verum

ex_inf_of Y,L ) & ( for x being Element of L st x in F holds

ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds

"/\" (Y,L) in F ) holds

F is filtered

let X, F be Subset of L; :: thesis: ( ( for Y being finite Subset of X st Y <> {} holds

ex_inf_of Y,L ) & ( for x being Element of L st x in F holds

ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds

"/\" (Y,L) in F ) implies F is filtered )

assume that

A1: for Y being finite Subset of X st Y <> {} holds

ex_inf_of Y,L and

A2: for x being Element of L st x in F holds

ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) ) and

A3: for Y being finite Subset of X st Y <> {} holds

"/\" (Y,L) in F ; :: thesis: F is filtered

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( x in F & y in F implies ex z being Element of L st

( z in F & z <= x & z <= y ) )

assume A4: x in F ; :: thesis: ( not y in F or ex z being Element of L st

( z in F & z <= x & z <= y ) )

then consider Y1 being finite Subset of X such that

A5: ex_inf_of Y1,L and

A6: x = "/\" (Y1,L) by A2;

assume y in F ; :: thesis: ex z being Element of L st

( z in F & z <= x & z <= y )

then consider Y2 being finite Subset of X such that

A7: ex_inf_of Y2,L and

A8: y = "/\" (Y2,L) by A2;

take z = "/\" ((Y1 \/ Y2),L); :: thesis: ( z in F & z <= x & z <= y )

A9: ( ( Y1 = {} & Y2 = {} & {} \/ {} = {} ) or Y1 \/ Y2 <> {} ) ;

hence z in F by A3, A4, A6; :: thesis: ( z <= x & z <= y )

ex_inf_of Y1 \/ Y2,L by A1, A5, A9;

hence ( z <= x & z <= y ) by A5, A6, A7, A8, XBOOLE_1:7, YELLOW_0:35; :: thesis: verum