defpred S₁[ set ] means ex y being set st
( y = $1 & y c= A & y is finite );
consider P being set such that
A1: for x being set holds
( x in P iff ( x in bool A & S₁[x] ) ) from XBOOLE_0:sch 1();
{} c= A by XBOOLE_1:2;
then reconsider Q = P as non empty set by A1;
for X, Y being set st X in Q & Y in Q holds
( X \/ Y in Q & X \ Y in Q )

proof

let X, Y be set ; :: thesis: ( X in Q & Y in Q implies ( X \/ Y in Q & X \ Y in Q ) )
assume that
A2: X in Q and
A3: Y in Q ; :: thesis: ( X \/ Y in Q & X \ Y in Q )
consider Z1 being set such that
A4: Z1 = X and
A5: Z1 c= A and
A6: Z1 is finite by A1, A2;
consider Z2 being set such that
A7: Z2 = Y and
A8: Z2 c= A and
A9: Z2 is finite by A1, A3;
A10: Z1 \ Z2 c= A by A5, XBOOLE_1:1;
Z1 \/ Z2 c= A by A5, A8, XBOOLE_1:8;
hence ( X \/ Y in Q & X \ Y in Q ) by A1, A4, A6, A7, A9, A10; :: thesis: verum

end;

then reconsider R = Q as non empty preBoolean set by Th10;
for X being set holds
( X in R iff ( X c= A & X is finite ) )

proof

let X be set ; :: thesis: ( X in R iff ( X c= A & X is finite ) )
thus ( X in R implies ( X c= A & X is finite ) ) :: thesis: ( X c= A & X is finite implies X in R )

proof

assume X in R ; :: thesis: ( X c= A & X is finite )
then ex Y being set st
( Y = X & Y c= A & Y is finite ) by A1;
hence ( X c= A & X is finite ) ; :: thesis: verum

end;

thus ( X c= A & X is finite implies X in R ) by A1; :: thesis: verum

end;

hence ex b₁ being preBoolean set st
for X being set holds
( X in b₁ iff ( X c= A & X is finite ) ) ; :: thesis: verum