A4: F₄() is finite ;
A5: P₁[ {} ] by A1;
A6: for x, B being set st x in F₄() & B c= F₄() & P₁[B] holds
P₁[B \/ {x}]

proof

let A, C1 be set ; :: thesis: ( A in F₄() & C1 c= F₄() & P₁[C1] implies P₁[C1 \/ {A}] )
assume that
A7: A in F₄() and
A8: C1 c= F₄() and
A9: P₁[C1] ; :: thesis: P₁[C1 \/ {A}]
reconsider A9 = A as Cell of F₃(),F₂() by A7;
reconsider C19 = C1 as Chain of F₃(),F₂() by A8, XBOOLE_1:1;

per cases ( A in C1 or not A in C1 ) ;

suppose A in C1 ; :: thesis: P₁[C1 \/ {A}]

then {A} c= C1 by ZFMISC_1:31;
hence P₁[C1 \/ {A}] by A9, XBOOLE_1:12; :: thesis: verum

end;

suppose A10: not A in C1 ; :: thesis: P₁[C1 \/ {A}]

now :: thesis: for A9 being object holds not A9 in C1 /\ {A}

let A9 be object ; :: thesis: not A9 in C1 /\ {A}
assume A11: A9 in C1 /\ {A} ; :: thesis: contradiction
then A12: A9 in C1 by XBOOLE_0:def 4;
A9 in {A} by A11, XBOOLE_0:def 4;
hence contradiction by A10, A12, TARSKI:def 1; :: thesis: verum

end;

then C1 /\ {A} = {} by XBOOLE_0:def 1;
then A13: C19 + {A9} = (C1 \/ {A}) \ {} by XBOOLE_1:101
.= C1 \/ {A} ;
A14: P₁[{A9}] by A2, A7;
{A} c= F₄() by A7, ZFMISC_1:31;
hence P₁[C1 \/ {A}] by A3, A8, A9, A13, A14; :: thesis: verum

end;

end;

end;

thus P₁[F₄()] from FINSET_1:sch 2(A4, A5, A6); :: thesis: verum