let X, Y be finite set ; :: thesis: ( Y c= X implies card (X \ Y) = (card X) - (card Y) )
assume A1: Y c= X ; :: thesis: card (X \ Y) = (card X) - (card Y)
A2: Y is finite ;
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 A3: S₁[ {} ] by CARD_1:47;
A4: 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 A5: ( X1 in Y & Z c= Y & S₁[Z] & not S₁[Z \/ {X1}] ) ; :: thesis: contradiction

now

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

end;

then A6: ( X \ Z is finite & not X1 in Z & X1 in X & Z is finite & card {X1} = 1 ) by A1, A5, CARD_1:50;
reconsider Z1 = Z as finite set by A5;
A7: ( X1 in X \ Z & X \ Z, card (X \ Z) are_equipotent & (card Z1) + (card {X1}) = card (Z1 \/ {X1}) ) by A6, Th54, CARD_1:def 5, XBOOLE_0:def 5;
then card (X \ Z) <> {} ;
then consider m being Nat such that
A8: card (X \ Z) = m + 1 by NAT_1:6;
U: m + 1 = succ m by NAT_1:39;
then Z: m in m + 1 by ORDINAL1:10;
T: m = (m + 1) \ {m} by U, ORDINAL1:52;
X \ (Z \/ {X1}) = (X \ Z) \ {X1} by XBOOLE_1:41;
then Y1: X \ (Z \/ {X1}),m are_equipotent by A7, A8, Z, T, CARD_1:61;
card {X1} = 1 by CARD_1:50;
then card (X \ (Z \/ {X1})) = (card X) - (card (Z1 \/ {X1})) by A5, A7, A8, Y1, CARD_1:def 5;
hence contradiction by A5; :: thesis: verum

end;

S₁[Y] from FINSET_1:sch 2(A2, A3, A4);
hence card (X \ Y) = (card X) - (card Y) ; :: thesis: verum