let X, Y be finite set ; :: thesis: ( Y c= X implies card (X \ Y) = (card X) - (card Y) )
defpred S₁[ set ] means ex S being finite set st
( S = $1 & card (X \ S) = (card X) - (card S) );
( (card X) - 0 = card X & X \ {} = X ) ;
then A1: S₁[ {} ] by CARD_1:27;
assume A2: Y c= X ; :: thesis: card (X \ Y) = (card X) - (card Y)
A3: for X1, Z being set st X1 in Y & Z c= Y & S₁[Z] holds
S₁[Z \/ {X1}]

proof

let X1, Z be set ; :: thesis: ( X1 in Y & Z c= Y & S₁[Z] implies S₁[Z \/ {X1}] )
assume that
A4: X1 in Y and
A5: Z c= Y and
A6: S₁[Z] and
A7: not S₁[Z \/ {X1}] ; :: thesis: contradiction
A8: card {X1} = 1 by CARD_1:30;

A9: now :: thesis: ( X1 in Z implies S₁[Z \/ {X1}] )

assume X1 in Z ; :: thesis: S₁[Z \/ {X1}]
then {X1} c= Z by ZFMISC_1:31;
then Z = Z \/ {X1} by XBOOLE_1:12;
hence S₁[Z \/ {X1}] by A6; :: thesis: verum

end;

then A10: X1 in X \ Z by A2, A4, A7, XBOOLE_0:def 5;
then consider m being Nat such that
A11: card (X \ Z) = m + 1 by NAT_1:6;
reconsider Z1 = Z as finite set by A5;
A12: ( X \ Z, card (X \ Z) are_equipotent & X \ (Z \/ {X1}) = (X \ Z) \ {X1} ) by CARD_1:def 2, XBOOLE_1:41;
card {X1} = 1 by CARD_1:30;
then A13: (card Z1) + (card {X1}) = card (Z1 \/ {X1}) by A7, A9, Th40;
Segm (m + 1) = succ (Segm m) by NAT_1:38;
then ( m in m + 1 & m = (m + 1) \ {m} ) by ORDINAL1:6, ORDINAL1:37;
then X \ (Z \/ {X1}),m are_equipotent by A10, A11, A12, CARD_1:34;
then card (X \ (Z \/ {X1})) = (card X) - (card (Z1 \/ {X1})) by A6, A13, A11, A8, CARD_1:def 2;
hence contradiction by A7; :: thesis: verum

end;

A14: Y is finite ;
S₁[Y] from FINSET_1:sch 2(A14, A1, A3);
hence card (X \ Y) = (card X) - (card Y) ; :: thesis: verum