let n be 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 Segm (n + 1) ) by A4, ORDINAL1:16;
then ( n c= card (a /\ b) or card (a \/ b) in succ (Segm n) ) by NAT_1:38;
then A5: ( n c= card (a /\ b) or card (a \/ b) c= n ) by ORDINAL1:22;
( n c= card (a \/ b) & card (a /\ b) c= n ) by A2, CARD_1:11, 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_2:102, XBOOLE_1:17;
hence contradiction by A1; :: thesis: verum