let X be non empty set ; :: thesis:
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:
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:

A2: now :: thesis:

let x, B be set ; :: thesis:
assume that
A3: x in Y and
B c= Y ; :: thesis:
assume S₁[B] ; :: thesis:
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:

proof

take c ; :: thesis:

hereby :: thesis:

let y be set ; :: thesis:
assume y in B \/ {x} ; :: thesis:
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:

end;

thus c in X by A7; :: thesis:

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: