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 )

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

set x = the Element of X;

reconsider x = the Element of X as Element of L ;

( 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 A5:
for Y being finite Subset of X st Y <> {} holds
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;"/\" (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

"/\" (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 )

hence
X is filtered
by Th2; :: thesis: verum( x in X & x is_<=_than Y )

let Y be finite Subset of X; :: thesis: ex x being Element of L st

( b_{2} in X & b_{2} is_<=_than x )

end;( b

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

end;

suppose
Y = {}
; :: thesis: ex x being Element of L st

( b_{2} in X & b_{2} is_<=_than x )

( b

then
x is_<=_than Y
;

hence ex x being Element of L st

( x in X & x is_<=_than Y ) ; :: thesis: verum

end;hence ex x being Element of L st

( x in X & x is_<=_than Y ) ; :: thesis: verum

suppose A6:
Y <> {}
; :: thesis: ex x being Element of L st

( b_{2} in X & b_{2} is_<=_than x )

( b

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