let k, n be Nat; :: thesis: for a, b being set st card a = n + k & card b = n + k holds
( card (a /\ b) = n iff card (a \/ b) = n + (2 * k) )
let a, b be set ; :: thesis: ( card a = n + k & card b = n + k implies ( card (a /\ b) = n iff card (a \/ b) = n + (2 * k) ) )
assume that
A1: card a = n + k and
A2: card b = n + k ; :: thesis: ( card (a /\ b) = n iff card (a \/ b) = n + (2 * k) )
A3: a is finite by A1;
A4: b is finite by A2;
thus ( card (a /\ b) = n implies card (a \/ b) = n + (2 * k) ) :: thesis: ( card (a \/ b) = n + (2 * k) implies card (a /\ b) = n )
proof
assume card (a /\ b) = n ; :: thesis: card (a \/ b) = n + (2 * k)
then card (a \/ b) = ((n + k) + (n + k)) - n by A1, A2, A3, A4, CARD_2:45;
hence card (a \/ b) = n + (2 * k) ; :: thesis: verum
end;
thus ( card (a \/ b) = n + (2 * k) implies card (a /\ b) = n ) :: thesis: verum
proof
reconsider m = card (a /\ b) as Nat by A3;
assume card (a \/ b) = n + (2 * k) ; :: thesis: card (a /\ b) = n
then n + (2 * k) = ((n + k) + (n + k)) - m by A1, A2, A3, A4, CARD_2:45;
hence card (a /\ b) = n ; :: thesis: verum
end;