defpred S_{1}[ set ] means P_{1}[F_{2}() \/ $1];

set D = F_{1}() \ F_{2}();

A4: F_{1}() \ F_{2}() is finite
by A1;

A5: for x, E being set st x in F_{1}() \ F_{2}() & E c= F_{1}() \ F_{2}() & S_{1}[E] holds

S_{1}[E \/ {x}]
_{1}[ {} ]
by A2;

S_{1}[F_{1}() \ F_{2}()]
from FINSET_1:sch 2(A4, A10, A5);

hence P_{1}[F_{1}()]
by XBOOLE_1:45; :: thesis: verum

set D = F

A4: F

A5: for x, E being set st x in F

S

proof

A10:
S
let x, E be set ; :: thesis: ( x in F_{1}() \ F_{2}() & E c= F_{1}() \ F_{2}() & S_{1}[E] implies S_{1}[E \/ {x}] )

assume that

A6: x in F_{1}() \ F_{2}()
and

A7: E c= F_{1}() \ F_{2}()
and

A8: S_{1}[E]
; :: thesis: S_{1}[E \/ {x}]

set C = F_{2}() \/ E;

F_{2}() \/ E c= F_{2}() \/ (F_{1}() \ F_{2}())
by A7, XBOOLE_1:9;

then F_{2}() \/ E c= F_{1}()
by XBOOLE_1:45;

then P_{1}[(F_{2}() \/ E) \/ {x}]
by A3, A6, A8, XBOOLE_1:7;

hence S_{1}[E \/ {x}]
by XBOOLE_1:4; :: thesis: verum

end;assume that

A6: x in F

A7: E c= F

A8: S

set C = F

F

then F

then P

hence S

S

hence P