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 ) )

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

( ( 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

A54:
x1 <> x3
by A10, A12, A22, A18, XBOOLE_0:def 4;
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 ) )

end;A27: ( x1 in c implies ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) )

proof

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

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

then A32: (a /\ c) \ {x1} c= (a /\ b) /\ c by XBOOLE_1:16;

A33: a /\ b misses {x1,x2}

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

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;proof

then A30:
(a /\ b) /\ c c= (a /\ c) \ {x1}
by A16, XBOOLE_1:17, XBOOLE_1:86;
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 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

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

proof

then
(a /\ c) \ {x1} c= (a /\ c) /\ b
by XBOOLE_1:19;
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;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

then A32: (a /\ c) \ {x1} c= (a /\ b) /\ c by XBOOLE_1:16;

A33: a /\ b misses {x1,x2}

proof

assume
x1 in c
; :: thesis: ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n )
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;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

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

then A42:
c c= a \/ b
by A15, A11, A19, XBOOLE_1:13;
assume A39:
x2 <> x3
; :: thesis: contradiction

b /\ c c= (a /\ b) /\ c

then (- 2) + n <= (- 3) + n by A6, A38, NAT_1:39;

hence contradiction by XREAL_1:6; :: thesis: verum

end;b /\ c c= (a /\ b) /\ c

proof

then
Segm (card (b /\ c)) c= Segm (card ((a /\ b) /\ c))
by CARD_1:11;
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;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

then (- 2) + n <= (- 3) + n by A6, A38, NAT_1:39;

hence contradiction by XREAL_1:6; :: thesis: verum

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

proof

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
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} )

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}

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;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

then
a /\ c c= a \ {x1}
by XBOOLE_1:17, XBOOLE_1:86;
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) /\ {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

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

a \/ b = (a /\ b) \/ ({x1} \/ {x2})
by A13, A17, XBOOLE_1:5;
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;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

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

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

proof

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
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;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