let n be Nat; 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 ; ( 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
; ( ( 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
;
( ( 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}
then A30:
(a /\ b) /\ c c= (a /\ c) \ {x1}
by A16, XBOOLE_1:17, XBOOLE_1:86;
(a /\ c) \ {x1} c= b
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}
assume
x1 in c
;
( 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
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;
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
;
( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 )
A46:
(
a /\ c misses {x1} &
a /\ b misses {x1} )
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}
;
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;
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;
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;
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
;
( 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;
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; verum