let n be Element of NAT ; :: thesis:
let a, b, c be set ; :: thesis:
assume A1: ( card a = n - 1 & card b = n - 1 & card c = n - 1 & card (a /\ b) = n - 2 & card (a /\ c) = n - 2 & card (b /\ c) = n - 2 & 2 <= n ) ; :: thesis:
then ( 2 <= n + 1 & 1 <= 1 ) by NAT_1:13;
then 2 - 1 <= (n + 1) - 1 by XREAL_1:15;
then A2: ( n - 2 is Element of NAT & n - 1 is Element of NAT ) by A1, NAT_1:21;
A3: ( a /\ b c= a & a /\ b c= b & a /\ c c= c & a /\ c c= a & a is finite & b is finite & c is finite & a /\ b is finite & a /\ c is finite & b /\ c is finite ) by A1, A2, XBOOLE_1:17;
then A4: ( card (a \ (a /\ b)) = (n - 1) - (n - 2) & card (c \ (a /\ c)) = (n - 1) - (n - 2) & card (b \ (a /\ b)) = (n - 1) - (n - 2) ) by A1, CARD_2:63;
then consider x1 being set such that
A5: {x1} = a \ (a /\ b) by CARD_2:60;
consider x2 being set such that
A6: {x2} = b \ (a /\ b) by A4, CARD_2:60;
consider x3 being set such that
A7: {x3} = c \ (a /\ c) by A4, CARD_2:60;
A8: ( a = (a /\ b) \/ {x1} & b = (a /\ b) \/ {x2} & c = (a /\ c) \/ {x3} ) by A3, A5, A6, A7, XBOOLE_1:45;
A9: ( x1 in {x1} & x2 in {x2} & x3 in {x3} ) by TARSKI:def 1;
then A10: ( x1 in a & not x1 in a /\ b & x2 in b & not x2 in a /\ b & x3 in c & not x3 in a /\ c ) by A5, A6, A7, XBOOLE_0:def 5;
then A11: ( not x1 in b & not x2 in a & x1 <> x2 & not x3 in a & x1 <> x3 ) by XBOOLE_0:def 4;
A12: ( (a /\ b) /\ c = (a /\ c) /\ b & (a /\ b) /\ c = (b /\ c) /\ a & (a /\ c) /\ b c= a /\ c & (b /\ c) /\ a c= b /\ c ) by XBOOLE_1:16, XBOOLE_1:17;
A13: ( n = 2 implies ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) )

proof

assume A14: n = 2 ; :: thesis:
then A15: ( a /\ b = {} & (a /\ b) /\ c c= a /\ b & a /\ b c= {} ) by A1, XBOOLE_1:17;
card ((a \/ b) \/ c) = n + 1

proof

A16: ( (a /\ b) /\ c = a /\ c & (a /\ b) /\ c = b /\ c & (a /\ b) /\ c = a /\ b & x3 in {x3} ) by A1, A15, TARSKI:def 1;
then A17: ( not x3 in a & not x3 in b & x1 <> x3 & x2 <> x3 ) by A10, XBOOLE_0:def 4;
(a \/ b) \/ c = ((a /\ b) /\ c) \/ ({x1,x2} \/ {x3}) by A5, A6, A7, A15, A16, ENUMSET1:41;
then (a \/ b) \/ c = ((a /\ b) /\ c) \/ {x1,x2,x3} by ENUMSET1:43;
hence card ((a \/ b) \/ c) = n + 1 by A11, A14, A15, A17, CARD_2:77; :: thesis:

end;

hence ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) by A14, A15; :: thesis:

end;

( not 3 <= n or ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) or ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) )

proof

assume 3 <= n ; :: thesis:
then A18: n - 3 is Element of NAT by NAT_1:21;
A19: ( x1 in c implies ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) )

proof

assume x1 in c ; :: thesis:
then x1 in a /\ c by A5, A9, XBOOLE_0:def 4;
then ( {x1} c= a /\ c & card {x1} = 1 ) by CARD_1:50, ZFMISC_1:37;
then A20: ( card ((a /\ c) \ {x1}) = (n - 2) - 1 & card (a \ (a /\ c)) = (n - 1) - (n - 2) ) by A1, A3, CARD_2:63;
A21: (a /\ c) \ {x1} c= b

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in (a /\ c) \ {x1} ; :: thesis:
then ( z in a /\ c & not z in {x1} ) by XBOOLE_0:def 5;
then ( ( z in a & not z in a \ (a /\ b) & not z in a ) or z in a /\ b ) by A5, XBOOLE_0:def 4, XBOOLE_0:def 5;
hence z in b by XBOOLE_0:def 4; :: thesis:

end;

(a /\ b) /\ c misses {x1}

proof

assume (a /\ b) /\ c meets {x1} ; :: thesis:
then not ((a /\ b) /\ c) /\ {x1} = {} by XBOOLE_0:def 7;
then consider x being set such that
A22: x in ((a /\ b) /\ c) /\ {x1} by XBOOLE_0:def 1;
A23: ( x in (a /\ b) /\ c & x in {x1} ) by A22, XBOOLE_0:def 4;
then ( x in (a /\ c) /\ b & x = x1 ) by TARSKI:def 1, XBOOLE_1:16;
hence contradiction by A10, A23, XBOOLE_0:def 4; :: thesis:

end;

then A24: (a /\ b) /\ c c= (a /\ c) \ {x1} by A12, XBOOLE_1:86;
(a /\ c) \ {x1} c= (a /\ c) /\ b by A21, XBOOLE_1:19;
then A25: (a /\ c) \ {x1} c= (a /\ b) /\ c by XBOOLE_1:16;
then A26: card ((a /\ b) /\ c) = n - 3 by A20, A24, XBOOLE_0:def 10;
x3 = x2

proof

assume A27: x2 <> x3 ; :: thesis:
b /\ c c= (a /\ b) /\ c

proof

let z1 be set ; :: according to TARSKI:def 3 :: thesis:
assume z1 in b /\ c ; :: thesis:
then ( z1 in b & z1 in c ) by XBOOLE_0:def 4;
then ( ( z1 in a /\ b or z1 in {x2} ) & ( z1 in a /\ c or z1 in {x3} ) ) by A8, XBOOLE_0:def 3;
then ( ( z1 in a /\ b or z1 = x2 ) & ( z1 in a /\ c or z1 = x3 ) ) by TARSKI:def 1;
then ( ( ( z1 in a /\ b or z1 in {x2} ) & z1 in a /\ c ) or ( z1 in a /\ b & ( z1 in a /\ c or z1 in {x3} ) ) ) by A27, TARSKI:def 1;
hence z1 in (a /\ b) /\ c by A3, A6, A7, A12, XBOOLE_0:def 4; :: thesis:

end;

then card (b /\ c) c= card ((a /\ b) /\ c) by CARD_1:27;
then (- 2) + n <= (- 3) + n by A1, A18, A26, NAT_1:40;
hence contradiction by XREAL_1:8; :: thesis:

end;

then A28: ( c c= a \/ b & a \/ b = (a /\ b) \/ ({x1} \/ {x2}) ) by A3, A6, A8, XBOOLE_1:5, XBOOLE_1:13;
then A29: ( (a \/ b) \/ c = a \/ b & a \/ b = (a /\ b) \/ {x1,x2} & card {x1,x2} = 2 ) by A11, CARD_2:76, ENUMSET1:41, XBOOLE_1:12;
a /\ b misses {x1,x2}

proof

assume a /\ b meets {x1,x2} ; :: thesis:
then (a /\ b) /\ {x1,x2} <> {} by XBOOLE_0:def 7;
then consider z1 being set such that
A30: z1 in (a /\ b) /\ {x1,x2} by XBOOLE_0:def 1;
( z1 in a /\ b & z1 in {x1,x2} ) by A30, XBOOLE_0:def 4;
hence contradiction by A10, TARSKI:def 2; :: thesis:

end;

then card (a \/ b) = (n - 2) + 2 by A1, A3, A29, CARD_2:53;
hence ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) by A20, A24, A25, A28, XBOOLE_0:def 10, XBOOLE_1:12; :: thesis:

end;

( not x1 in c implies ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) )

proof

assume A31: not x1 in c ; :: thesis:
( a /\ c misses {x1} & a /\ b misses {x1} )

proof

assume ( not a /\ c misses {x1} or not a /\ b misses {x1} ) ; :: thesis:
then ( (a /\ c) /\ {x1} <> {} or (a /\ b) /\ {x1} <> {} ) by XBOOLE_0:def 7;
then consider z2 being set such that
A32: ( z2 in (a /\ c) /\ {x1} or z2 in (a /\ b) /\ {x1} ) by XBOOLE_0:def 1;
( ( z2 in a /\ c & z2 in {x1} ) or ( z2 in a /\ b & z2 in {x1} ) ) by A32, XBOOLE_0:def 4;
then ( ( z2 in a & z2 in c & z2 = x1 ) or ( z2 in a /\ b & z2 = x1 ) ) by TARSKI:def 1, XBOOLE_0:def 4;
hence contradiction by A5, A9, A31, XBOOLE_0:def 5; :: thesis:

end;

then ( a /\ c c= a \ {x1} & a /\ b c= a \ {x1} & a \ {x1} c= a & {x1} c= a & card (a \ {x1}) = (n - 1) - 1 & a \ {x1} is finite ) by A1, A3, A4, A5, CARD_2:63, XBOOLE_1:86;
then A33: ( a /\ c = a \ {x1} & a /\ b = a \ {x1} ) by A1, CARD_FIN:1;
then (a /\ b) /\ (a /\ c) = a /\ b ;
then ((b /\ a) /\ a) /\ c = a /\ b by XBOOLE_1:16;
then A34: (b /\ (a /\ a)) /\ c = a /\ b by XBOOLE_1:16;
then A35: (a /\ b) /\ c = b /\ c by A1, A3, A12, CARD_FIN:1;
a \/ b = (a /\ b) \/ ({x1} \/ {x2}) by A8, XBOOLE_1:5;
then a \/ b = (a /\ b) \/ {x1,x2} by ENUMSET1:41;
then (a \/ b) \/ c = (a /\ b) \/ ({x1,x2} \/ {x3}) by A8, A33, XBOOLE_1:5;
then A36: (a \/ b) \/ c = (a /\ b) \/ {x1,x2,x3} by ENUMSET1:43;
( x1 <> x3 & x2 <> x3 ) by A10, A34, A35, XBOOLE_0:def 4;
then A37: card {x1,x2,x3} = 3 by A11, CARD_2:77;
a /\ b misses {x1,x2,x3}

proof

assume not a /\ b misses {x1,x2,x3} ; :: thesis:
then (a /\ b) /\ {x1,x2,x3} <> {} by XBOOLE_0:def 7;
then consider z3 being set such that
A38: z3 in (a /\ b) /\ {x1,x2,x3} by XBOOLE_0:def 1;
( z3 in a /\ b & z3 in {x1,x2,x3} ) by A38, XBOOLE_0:def 4;
hence contradiction by A10, A33, ENUMSET1:def 1; :: thesis:

end;

then card ((a \/ b) \/ c) = (n - 2) + 3 by A1, A3, A36, A37, CARD_2:53;
hence ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) by A1, A34; :: thesis:

end;

hence ( ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) or ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) ) by A19; :: thesis:

end;

hence ( ( not 3 <= n or ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) or ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) ) & ( n = 2 implies ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) ) ) by A13; :: thesis: