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

( 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