let n be Element of NAT ; :: thesis:
let a, b, c be set ; :: thesis:
assume that
A1: card a = n - 1 and
A2: card b = n - 1 and
A3: card c = n - 1 and
A4: card (a /\ b) = n - 2 and
A5: card (a /\ c) = n - 2 and
A6: card (b /\ c) = n - 2 and
A7: 2 <= n ; :: thesis:
2 <= n + 1 by A7, NAT_1:13;
then A8: 2 - 1 <= (n + 1) - 1 by XREAL_1:15;
then A9: a is finite by A1, NAT_1:21;
then A10: card (a \ (a /\ b)) = (n - 1) - (n - 2) by A1, A4, CARD_2:63, XBOOLE_1:17;
then consider x1 being set such that
A11: {x1} = a \ (a /\ b) by CARD_2:60;
A12: b is finite by A2, A8, NAT_1:21;
then card (b \ (a /\ b)) = (n - 1) - (n - 2) by A2, A4, CARD_2:63, XBOOLE_1:17;
then consider x2 being set such that
A13: {x2} = b \ (a /\ b) by CARD_2:60;
c is finite by A3, A8, NAT_1:21;
then card (c \ (a /\ c)) = (n - 1) - (n - 2) by A3, A5, CARD_2:63, XBOOLE_1:17;
then consider x3 being set such that
A14: {x3} = c \ (a /\ c) by CARD_2:60;
A15: a = (a /\ b) \/ {x1} by A11, XBOOLE_1:17, XBOOLE_1:45;
A16: (a /\ b) /\ c = (b /\ c) /\ a by XBOOLE_1:16;
A17: a /\ c c= a by XBOOLE_1:17;
A18: (a /\ b) /\ c = (a /\ c) /\ b by XBOOLE_1:16;
A19: b = (a /\ b) \/ {x2} by A13, XBOOLE_1:17, XBOOLE_1:45;
x3 in {x3} by TARSKI:def 1;
then A20: not x3 in a /\ c by A14, XBOOLE_0:def 5;
A21: c = (a /\ c) \/ {x3} by A14, XBOOLE_1:17, XBOOLE_1:45;
A22: x2 in {x2} by TARSKI:def 1;
then A23: not x2 in a /\ b by A13, XBOOLE_0:def 5;
A24: x1 in {x1} by TARSKI:def 1;
then A25: not x1 in a /\ b by A11, XBOOLE_0:def 5;
then A26: x1 <> x2 by A11, A13, A22, XBOOLE_0:def 4;
A27: a /\ b c= b by XBOOLE_1:17;
A28: ( 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 ) )

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

(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
A31: x in ((a /\ b) /\ c) /\ {x1} by XBOOLE_0:def 1;
x in {x1} by A31, XBOOLE_0:def 4;
then A32: x = x1 by TARSKI:def 1;
x in (a /\ b) /\ c by A31, XBOOLE_0:def 4;
hence contradiction by A25, A32, XBOOLE_0:def 4; :: thesis:

end;

then A33: (a /\ b) /\ c c= (a /\ c) \ {x1} by A18, XBOOLE_1:17, XBOOLE_1:86;
(a /\ c) \ {x1} c= b

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A34: z in (a /\ c) \ {x1} ; :: thesis:
then 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 A11, A34, XBOOLE_0:def 4, XBOOLE_0:def 5;
hence z in b by XBOOLE_0:def 4; :: thesis:

end;

then (a /\ c) \ {x1} c= (a /\ c) /\ b by XBOOLE_1:19;
then A35: (a /\ c) \ {x1} c= (a /\ b) /\ c by XBOOLE_1:16;
A36: 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
A37: z1 in (a /\ b) /\ {x1,x2} by XBOOLE_0:def 1;
( z1 in a /\ b & z1 in {x1,x2} ) by A37, XBOOLE_0:def 4;
hence contradiction by A25, A23, TARSKI:def 2; :: thesis:

end;

assume x1 in c ; :: thesis:
then x1 in a /\ c by A11, A24, XBOOLE_0:def 4;
then A38: {x1} c= a /\ c by ZFMISC_1:37;
a \/ b = (a /\ b) \/ ({x1} \/ {x2}) by A15, A19, XBOOLE_1:5;
then A39: a \/ b = (a /\ b) \/ {x1,x2} by ENUMSET1:41;
card {x1} = 1 by CARD_1:50;
then A40: card ((a /\ c) \ {x1}) = (n - 2) - 1 by A5, A9, A38, CARD_2:63;
then A41: card ((a /\ b) /\ c) = n - 3 by A33, A35, XBOOLE_0:def 10;
x3 = x2

proof

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

proof

let z1 be set ; :: according to TARSKI:def 3 :: thesis:
assume A43: z1 in b /\ c ; :: thesis:
then z1 in b by XBOOLE_0:def 4;
then ( z1 in a /\ b or z1 in {x2} ) by A19, XBOOLE_0:def 3;
then A44: ( z1 in a /\ b or z1 = x2 ) by TARSKI:def 1;
z1 in c by A43, XBOOLE_0:def 4;
then ( z1 in a /\ c or z1 in {x3} ) by A21, XBOOLE_0:def 3;
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 A42, A44, TARSKI:def 1;
hence z1 in (a /\ b) /\ c by A27, A13, A14, A18, 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 A6, A29, A41, NAT_1:40;
hence contradiction by XREAL_1:8; :: thesis:

end;

then A45: c c= a \/ b by A17, A13, A21, XBOOLE_1:13;
card {x1,x2} = 2 by A26, CARD_2:76;
then card (a \/ b) = (n - 2) + 2 by A4, A9, A39, A36, CARD_2:53;
hence ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) by A40, A33, A35, A45, 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

A46: x1 <> x3 by A11, A14, A24, A20, XBOOLE_0:def 4;
A47: card (a \ {x1}) = (n - 1) - 1 by A1, A9, A10, A11, CARD_2:63;
assume A48: not x1 in c ; :: thesis:
A49: ( 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
A50: ( 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 A50, 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 A11, A24, A48, XBOOLE_0:def 5; :: thesis:

end;

then a /\ c c= a \ {x1} by XBOOLE_1:17, XBOOLE_1:86;
then A51: a /\ c = a \ {x1} by A5, A9, A47, CARD_FIN:1;
a /\ b c= a \ {x1} by A49, XBOOLE_1:17, XBOOLE_1:86;
then A52: a /\ b = a \ {x1} by A4, A9, A47, CARD_FIN:1;
A53: 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
A54: z3 in (a /\ b) /\ {x1,x2,x3} by XBOOLE_0:def 1;
( z3 in a /\ b & z3 in {x1,x2,x3} ) by A54, XBOOLE_0:def 4;
hence contradiction by A25, A23, A20, A51, A52, ENUMSET1:def 1; :: thesis:

end;

a \/ b = (a /\ b) \/ ({x1} \/ {x2}) by A15, A19, XBOOLE_1:5;
then a \/ b = (a /\ b) \/ {x1,x2} by ENUMSET1:41;
then (a \/ b) \/ c = (a /\ b) \/ ({x1,x2} \/ {x3}) by A21, A51, A52, XBOOLE_1:5;
then A55: (a \/ b) \/ c = (a /\ b) \/ {x1,x2,x3} by ENUMSET1:43;
(a /\ b) /\ (a /\ c) = a /\ b by A51, A52;
then ((b /\ a) /\ a) /\ c = a /\ b by XBOOLE_1:16;
then A56: (b /\ (a /\ a)) /\ c = a /\ b by XBOOLE_1:16;
then (a /\ b) /\ c = b /\ c by A4, A6, A12, A16, CARD_FIN:1, XBOOLE_1:17;
then x2 <> x3 by A13, A14, A22, A23, A56, XBOOLE_0:def 4;
then card {x1,x2,x3} = 3 by A26, A46, CARD_2:77;
then card ((a \/ b) \/ c) = (n - 2) + 3 by A4, A9, A55, A53, CARD_2:53;
hence ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) by A4, A56; :: 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 A30; :: thesis:

end;

A57: x1 <> x3 by A11, A14, A24, A20, XBOOLE_0:def 4;
( n = 2 implies ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) )

proof

assume A58: n = 2 ; :: thesis:
then A59: a /\ b = {} by A4;
then (a /\ b) /\ c = a /\ c by A4, A5;
then (a \/ b) \/ c = ((a /\ b) /\ c) \/ ({x1,x2} \/ {x3}) by A11, A13, A14, A59, ENUMSET1:41;
then A60: (a \/ b) \/ c = ((a /\ b) /\ c) \/ {x1,x2,x3} by ENUMSET1:43;
(a /\ b) /\ c = b /\ c by A4, A6, A59;
then x2 <> x3 by A13, A14, A22, A59, XBOOLE_0:def 4;
hence ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) by A26, A57, A58, A59, A60, CARD_2:77; :: 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 A28; :: thesis: