let L be with_infima Poset; :: thesis: for X being non empty upper Subset of L holds
( X is filtered iff for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X )
let X be non empty upper Subset of L; :: thesis: ( X is filtered iff for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X )
thus ( X is filtered implies for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X ) :: thesis: ( ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X ) implies X is filtered )

proof

assume A1: X is filtered ; :: thesis: for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X
let Y be finite Subset of X; :: thesis: ( Y <> {} implies "/\" (Y,L) in X )
assume A2: Y <> {} ; :: thesis: "/\" (Y,L) in X
consider z being Element of L such that
A3: z in X and
A4: Y is_>=_than z by A1, Th2;
Y c= the carrier of L by XBOOLE_1:1;
then ex_inf_of Y,L by A2, YELLOW_0:55;
then "/\" (Y,L) >= z by A4, YELLOW_0:31;
hence "/\" (Y,L) in X by A3, Def20; :: thesis: verum

end;

assume A5: for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X ; :: thesis: X is filtered
set x = the Element of X;
reconsider x = the Element of X as Element of L ;

now :: thesis: for Y being finite Subset of X ex x being Element of L st
( x in X & x is_<=_than Y )

let Y be finite Subset of X; :: thesis: ex x being Element of L st
( b₂ in X & b₂ is_<=_than x )

per cases ( Y = {} or Y <> {} ) ;

suppose Y = {} ; :: thesis: ex x being Element of L st
( b₂ in X & b₂ is_<=_than x )

then x is_<=_than Y ;
hence ex x being Element of L st
( x in X & x is_<=_than Y ) ; :: thesis: verum

end;

suppose A6: Y <> {} ; :: thesis: ex x being Element of L st
( b₂ in X & b₂ is_<=_than x )

Y c= the carrier of L by XBOOLE_1:1;
then ex_inf_of Y,L by A6, YELLOW_0:55;
then "/\" (Y,L) is_<=_than Y by YELLOW_0:31;
hence ex x being Element of L st
( x in X & x is_<=_than Y ) by A5, A6; :: thesis: verum

end;

end;

end;

hence X is filtered by Th2; :: thesis: verum