A4: F4() is finite ;
A5: P1[ {} ] by A1;
A6: for x, B being set st x in F4() & B c= F4() & P1[B] holds
P1[B \/ {x}]
proof
let A, C1 be set ; :: thesis: ( A in F4() & C1 c= F4() & P1[C1] implies P1[C1 \/ {A}] )
assume that
A7: A in F4() and
A8: C1 c= F4() and
A9: P1[C1] ; :: thesis: P1[C1 \/ {A}]
reconsider A9 = A as Cell of F3(),F2() by A7;
reconsider C19 = C1 as Chain of F3(),F2() by A8, XBOOLE_1:1;
per cases ( A in C1 or not A in C1 ) ;
suppose A10: not A in C1 ; :: thesis: P1[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: P1[{A9}] by A2, A7;
{A} c= F4() by A7, ZFMISC_1:31;
hence P1[C1 \/ {A}] by A3, A8, A9, A13, A14; :: thesis: verum
end;
end;
end;
thus P1[F4()] from FINSET_1:sch 2(A4, A5, A6); :: thesis: verum