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 )

( 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

thus
( card (a \/ b) = n + (2 * k) implies card (a /\ b) = n )
:: thesis: verum
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;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