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 that
A1: a <> b and
A2: card a = n and
A3: card b = n and
A4: ( not card (a /\ b) in n or not n + 1 c= card (a \/ b) ) ; :: thesis: contradiction
( n c= card (a /\ b) or card (a \/ b) in n + 1 ) by A4, ORDINAL1:26;
then ( n c= card (a /\ b) or card (a \/ b) in succ n ) by NAT_1:39;
then A5: ( n c= card (a /\ b) or card (a \/ b) c= n ) by ORDINAL1:34;
( n c= card (a \/ b) & card (a /\ b) c= n ) by A2, CARD_1:27, XBOOLE_1:7, XBOOLE_1:17;
then A6: ( ( card a = card (a /\ b) & card (a /\ b) = card b ) or ( card (a \/ b) = card a & card (a \/ b) = card b ) ) by A2, A3, A5, XBOOLE_0:def 10;
A7: ( a c= a \/ b & b c= a \/ b ) by XBOOLE_1:7;
( a is finite set & b is finite set ) by A2, A3;
then ( ( a = a /\ b & b = a /\ b ) or ( a = a \/ b & b = a \/ b ) ) by A7, A6, CARD_FIN:1, XBOOLE_1:17;
hence contradiction by A1; :: thesis: verum