let n be Nat; :: thesis: for a, b, c being set st 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 holds
( ( 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 ) ) )
let a, b, c be set ; :: thesis: ( 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 implies ( ( 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 ) ) ) )
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: ( ( 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 ) ) )
2 <= n + 1 by A7, NAT_1:13;
then A8: 2 - 1 <= (n + 1) - 1 by XREAL_1:13;
then a is finite by A1, NAT_1:21;
then reconsider a = a as finite set ;
A9: card (a \ (a /\ b)) = (n - 1) - (n - 2) by A1, A4, CARD_2:44, XBOOLE_1:17;
then consider x1 being object such that
A10: {x1} = a \ (a /\ b) by CARD_2:42;
b is finite by A2, A8, NAT_1:21;
then reconsider b = b as finite set ;
card (b \ (a /\ b)) = (n - 1) - (n - 2) by A2, A4, CARD_2:44, XBOOLE_1:17;
then consider x2 being object such that
A11: {x2} = b \ (a /\ b) by CARD_2:42;
c is finite by A3, A8, NAT_1:21;
then card (c \ (a /\ c)) = (n - 1) - (n - 2) by A3, A5, CARD_2:44, XBOOLE_1:17;
then consider x3 being object such that
A12: {x3} = c \ (a /\ c) by CARD_2:42;
A13: a = (a /\ b) \/ {x1} by A10, XBOOLE_1:17, XBOOLE_1:45;
A14: (a /\ b) /\ c = (b /\ c) /\ a by XBOOLE_1:16;
A15: a /\ c c= a by XBOOLE_1:17;
A16: (a /\ b) /\ c = (a /\ c) /\ b by XBOOLE_1:16;
A17: b = (a /\ b) \/ {x2} by A11, XBOOLE_1:17, XBOOLE_1:45;
x3 in {x3} by TARSKI:def 1;
then A18: not x3 in a /\ c by A12, XBOOLE_0:def 5;
A19: c = (a /\ c) \/ {x3} by A12, XBOOLE_1:17, XBOOLE_1:45;
A20: x2 in {x2} by TARSKI:def 1;
then A21: not x2 in a /\ b by A11, XBOOLE_0:def 5;
A22: x1 in {x1} by TARSKI:def 1;
then A23: not x1 in a /\ b by A10, XBOOLE_0:def 5;
then A24: x1 <> x2 by A10, A11, A20, XBOOLE_0:def 4;
A25: a /\ b c= b by XBOOLE_1:17;
A26: ( 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: ( ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) or ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) )
A27: ( x1 in c implies ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) )

proof

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

proof

assume (a /\ b) /\ c meets {x1} ; :: thesis: contradiction
then not ((a /\ b) /\ c) /\ {x1} = {} by XBOOLE_0:def 7;
then consider x being object such that
A28: x in ((a /\ b) /\ c) /\ {x1} by XBOOLE_0:def 1;
x in {x1} by A28, XBOOLE_0:def 4;
then A29: x = x1 by TARSKI:def 1;
x in (a /\ b) /\ c by A28, XBOOLE_0:def 4;
hence contradiction by A23, A29, XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (a /\ c) \ {x1} or z in b )
assume A31: z in (a /\ c) \ {x1} ; :: thesis: z in b
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 A10, A31, XBOOLE_0:def 4, XBOOLE_0:def 5;
hence z in b by XBOOLE_0:def 4; :: thesis: verum

end;

then (a /\ c) \ {x1} c= (a /\ c) /\ b by XBOOLE_1:19;
then A32: (a /\ c) \ {x1} c= (a /\ b) /\ c by XBOOLE_1:16;
A33: a /\ b misses {x1,x2}

proof

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

end;

assume x1 in c ; :: thesis: ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n )
then x1 in a /\ c by A10, A22, XBOOLE_0:def 4;
then A35: {x1} c= a /\ c by ZFMISC_1:31;
a \/ b = (a /\ b) \/ ({x1} \/ {x2}) by A13, A17, XBOOLE_1:5;
then A36: a \/ b = (a /\ b) \/ {x1,x2} by ENUMSET1:1;
card {x1} = 1 by CARD_1:30;
then A37: card ((a /\ c) \ {x1}) = (n - 2) - 1 by A5, A35, CARD_2:44;
then A38: card ((a /\ b) /\ c) = n - 3 by A30, A32, XBOOLE_0:def 10;
x3 = x2

proof

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

proof

let z1 be object ; :: according to TARSKI:def 3 :: thesis: ( not z1 in b /\ c or z1 in (a /\ b) /\ c )
assume A40: z1 in b /\ c ; :: thesis: z1 in (a /\ b) /\ c
then z1 in b by XBOOLE_0:def 4;
then ( z1 in a /\ b or z1 in {x2} ) by A17, XBOOLE_0:def 3;
then A41: ( z1 in a /\ b or z1 = x2 ) by TARSKI:def 1;
z1 in c by A40, XBOOLE_0:def 4;
then ( z1 in a /\ c or z1 in {x3} ) by A19, 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 A39, A41, TARSKI:def 1;
hence z1 in (a /\ b) /\ c by A25, A11, A12, A16, XBOOLE_0:def 4; :: thesis: verum

end;

then Segm (card (b /\ c)) c= Segm (card ((a /\ b) /\ c)) by CARD_1:11;
then (- 2) + n <= (- 3) + n by A6, A38, NAT_1:39;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

then A42: c c= a \/ b by A15, A11, A19, XBOOLE_1:13;
card {x1,x2} = 2 by A24, CARD_2:57;
then card (a \/ b) = (n - 2) + 2 by A4, A36, A33, CARD_2:40;
hence ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) by A37, A30, A32, A42, XBOOLE_0:def 10, XBOOLE_1:12; :: thesis: verum

end;

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

proof

A43: x1 <> x3 by A10, A12, A22, A18, XBOOLE_0:def 4;
A44: card (a \ {x1}) = (n - 1) - 1 by A1, A9, A10, CARD_2:44;
assume A45: not x1 in c ; :: thesis: ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 )
A46: ( a /\ c misses {x1} & a /\ b misses {x1} )

proof

assume ( not a /\ c misses {x1} or not a /\ b misses {x1} ) ; :: thesis: contradiction
then ( (a /\ c) /\ {x1} <> {} or (a /\ b) /\ {x1} <> {} ) by XBOOLE_0:def 7;
then consider z2 being object such that
A47: ( 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 A47, 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 A10, A22, A45, XBOOLE_0:def 5; :: thesis: verum

end;

then a /\ c c= a \ {x1} by XBOOLE_1:17, XBOOLE_1:86;
then A48: a /\ c = a \ {x1} by A5, A44, CARD_2:102;
a /\ b c= a \ {x1} by A46, XBOOLE_1:17, XBOOLE_1:86;
then A49: a /\ b = a \ {x1} by A4, A44, CARD_2:102;
A50: a /\ b misses {x1,x2,x3}

proof

assume not a /\ b misses {x1,x2,x3} ; :: thesis: contradiction
then (a /\ b) /\ {x1,x2,x3} <> {} by XBOOLE_0:def 7;
then consider z3 being object such that
A51: z3 in (a /\ b) /\ {x1,x2,x3} by XBOOLE_0:def 1;
( z3 in a /\ b & z3 in {x1,x2,x3} ) by A51, XBOOLE_0:def 4;
hence contradiction by A23, A21, A18, A48, A49, ENUMSET1:def 1; :: thesis: verum

end;

a \/ b = (a /\ b) \/ ({x1} \/ {x2}) by A13, A17, XBOOLE_1:5;
then a \/ b = (a /\ b) \/ {x1,x2} by ENUMSET1:1;
then (a \/ b) \/ c = (a /\ b) \/ ({x1,x2} \/ {x3}) by A19, A48, A49, XBOOLE_1:5;
then A52: (a \/ b) \/ c = (a /\ b) \/ {x1,x2,x3} by ENUMSET1:3;
(a /\ b) /\ (a /\ c) = a /\ b by A48, A49;
then ((b /\ a) /\ a) /\ c = a /\ b by XBOOLE_1:16;
then A53: (b /\ (a /\ a)) /\ c = a /\ b by XBOOLE_1:16;
then (a /\ b) /\ c = b /\ c by A4, A6, A14, CARD_2:102, XBOOLE_1:17;
then x2 <> x3 by A11, A12, A20, A21, A53, XBOOLE_0:def 4;
then card {x1,x2,x3} = 3 by A24, A43, CARD_2:58;
then card ((a \/ b) \/ c) = (n - 2) + 3 by A4, A52, A50, CARD_2:40;
hence ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) by A4, A53; :: thesis: verum

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 A27; :: thesis: verum

end;

A54: x1 <> x3 by A10, A12, A22, A18, XBOOLE_0:def 4;
( n = 2 implies ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) )

proof

assume A55: n = 2 ; :: thesis: ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 )
then A56: a /\ b = {} by A4;
then (a /\ b) /\ c = a /\ c by A4, A5;
then (a \/ b) \/ c = ((a /\ b) /\ c) \/ ({x1,x2} \/ {x3}) by A10, A11, A12, A56, ENUMSET1:1;
then A57: (a \/ b) \/ c = ((a /\ b) /\ c) \/ {x1,x2,x3} by ENUMSET1:3;
(a /\ b) /\ c = b /\ c by A4, A6, A56;
then x2 <> x3 by A11, A12, A20, A56, XBOOLE_0:def 4;
hence ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) by A24, A54, A55, A56, A57, CARD_2:58; :: thesis: verum

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 A26; :: thesis: verum