let n be Element of NAT ; :: thesis: for a, b being set st a <> b & card a = n & card b = n holds
( card (a /\ b) in n & n + 1 c= card (a \/ b) )
let a, b be set ; :: thesis: ( a <> b & card a = n & card b = n implies ( card (a /\ b) in n & n + 1 c= card (a \/ b) ) )
assume A1: ( a <> b & card a = n & card b = n & ( not card (a /\ b) in n or not n + 1 c= card (a \/ b) ) ) ; :: thesis: contradiction
then ( n c= card (a /\ b) or card (a \/ b) in n + 1 ) by ORDINAL1:26;
then ( n c= card (a /\ b) or card (a \/ b) in succ n ) by NAT_1:39;
then A2: ( n c= card (a /\ b) or card (a \/ b) c= n ) by ORDINAL1:34;
A3: ( a c= a \/ b & b c= a \/ b & a /\ b c= a & a /\ b c= b ) by XBOOLE_1:7, XBOOLE_1:17;
then ( n c= card (a \/ b) & card (a /\ b) c= n ) by A1, CARD_1:27;
then A4: ( ( card a = card (a /\ b) & card (a /\ b) = card b ) or ( card (a \/ b) = card a & card (a \/ b) = card b ) ) by A1, A2, XBOOLE_0:def 10;
( a is finite set & b is finite set ) by A1;
then ( a \/ b is finite set & a /\ b is finite set ) ;
then ( ( a = a /\ b & b = a /\ b ) or ( a = a \/ b & b = a \/ b ) ) by A3, A4, CARD_FIN:1;
hence contradiction by A1; :: thesis: verum