let X, Y be finite set ; ( Y c= X implies card (X \ Y) = (card X) - (card Y) )
defpred S1[ 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:
S1[ {} ]
by CARD_1:27;
assume A2:
Y c= X
; card (X \ Y) = (card X) - (card Y)
A3:
for X1, Z being set st X1 in Y & Z c= Y & S1[Z] holds
S1[Z \/ {X1}]
proof
let X1,
Z be
set ;
( X1 in Y & Z c= Y & S1[Z] implies S1[Z \/ {X1}] )
assume that A4:
X1 in Y
and A5:
Z c= Y
and A6:
S1[
Z]
and A7:
not
S1[
Z \/ {X1}]
;
contradiction
A8:
card {X1} = 1
by CARD_1:30;
A9:
now ( X1 in Z implies S1[Z \/ {X1}] )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;
verum
end;
A14:
Y is finite
;
S1[Y]
from FINSET_1:sch 2(A14, A1, A3);
hence
card (X \ Y) = (card X) - (card Y)
; verum