let X be non empty set ; :: thesis: ( ( for a, b being set st a in X & b in X holds
ex c being set st
( c c= a /\ b & c in X ) ) implies X is c=filtered )
assume A1: for a, b being set st a in X & b in X holds
ex c being set st
( c c= a /\ b & c in X ) ; :: thesis: X is c=filtered
set a = the Element of X;
defpred S₁[ set ] means ex a being set st
( ( for y being set st y in $1 holds
a c= y ) & a in X );
let Y be finite Subset of X; :: according to COHSP_1:def 5 :: thesis: ex a being set st
( ( for y being set st y in Y holds
a c= y ) & a in X )

A2: now :: thesis: for x, B being set st x in Y & B c= Y & S₁[B] holds
S₁[B \/ {x}]

let x, B be set ; :: thesis: ( x in Y & B c= Y & S₁[B] implies S₁[B \/ {x}] )
assume that
A3: x in Y and
B c= Y ; :: thesis: ( S₁[B] implies S₁[B \/ {x}] )
assume S₁[B] ; :: thesis: S₁[B \/ {x}]
then consider a being set such that
A4: for y being set st y in B holds
a c= y and
A5: a in X ;
consider c being set such that
A6: c c= a /\ x and
A7: c in X by A1, A3, A5;
A8: ( a /\ x c= a & a /\ x c= x ) by XBOOLE_1:17;
thus S₁[B \/ {x}] :: thesis: verum

proof

take c ; :: thesis: ( ( for y being set st y in B \/ {x} holds
c c= y ) & c in X )

hereby :: thesis: c in X

let y be set ; :: thesis: ( y in B \/ {x} implies c c= y )
assume y in B \/ {x} ; :: thesis: c c= y
then ( y in B or y in {x} ) by XBOOLE_0:def 3;
then ( ( a c= y & c c= a ) or ( y = x & c c= x ) ) by A4, A6, A8, TARSKI:def 1;
hence c c= y ; :: thesis: verum

end;

thus c in X by A7; :: thesis: verum

end;

end;

for y being set st y in {} holds
the Element of X c= y ;
then A9: S₁[ {} ] ;
A10: Y is finite ;
thus S₁[Y] from FINSET_1:sch 2(A10, A9, A2); :: thesis: verum