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 & 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
A6: ( ex_inf_of Y2,L & y = "/\" Y2,L ) by A2;
take z = "/\" (Y1 \/ Y2),L; :: thesis: ( z in F & z <= x & z <= y )
A7: ( ( Y1 = {} & Y2 = {} & {} \/ {} = {} ) or Y1 \/ Y2 <> {} ) ;
hence z in F by A3, A4, A5; :: thesis: ( z <= x & z <= y )
( ex_inf_of Y1 \/ Y2,L & Y1 c= Y1 \/ Y2 & Y2 c= Y1 \/ Y2 ) by A1, A5, A7, XBOOLE_1:7;
hence ( z <= x & z <= y ) by A5, A6, YELLOW_0:35; :: thesis: verum