A4:
F_{4}() is finite
;

A5: P_{1}[ {} ]
by A1;

A6: for x, B being set st x in F_{4}() & B c= F_{4}() & P_{1}[B] holds

P_{1}[B \/ {x}]
_{1}[F_{4}()]
from FINSET_1:sch 2(A4, A5, A6); :: thesis: verum

A5: P

A6: for x, B being set st x in F

P

proof

thus
P
let A, C1 be set ; :: thesis: ( A in F_{4}() & C1 c= F_{4}() & P_{1}[C1] implies P_{1}[C1 \/ {A}] )

assume that

A7: A in F_{4}()
and

A8: C1 c= F_{4}()
and

A9: P_{1}[C1]
; :: thesis: P_{1}[C1 \/ {A}]

reconsider A9 = A as Cell of F_{3}(),F_{2}() by A7;

reconsider C19 = C1 as Chain of F_{3}(),F_{2}() by A8, XBOOLE_1:1;

end;assume that

A7: A in F

A8: C1 c= F

A9: P

reconsider A9 = A as Cell of F

reconsider C19 = C1 as Chain of F

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

end;

suppose A10:
not A in C1
; :: thesis: P_{1}[C1 \/ {A}]

then A13: C19 + {A9} = (C1 \/ {A}) \ {} by XBOOLE_1:101

.= C1 \/ {A} ;

A14: P_{1}[{A9}]
by A2, A7;

{A} c= F_{4}()
by A7, ZFMISC_1:31;

hence P_{1}[C1 \/ {A}]
by A3, A8, A9, A13, A14; :: thesis: verum

end;

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

then
C1 /\ {A} = {}
by XBOOLE_0:def 1;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;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

then A13: C19 + {A9} = (C1 \/ {A}) \ {} by XBOOLE_1:101

.= C1 \/ {A} ;

A14: P

{A} c= F

hence P