set B = Benzene ;
let a be Element of Benzene; ( ( a = 0 implies a ` = 3 ) & ( a = 3 implies a ` = 0 ) & ( a = 1 implies a ` = 3 \ 1 ) & ( a = 3 \ 1 implies a ` = 1 ) & ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
reconsider c = a as Subset of 3 by Th10;
A1:
a ` c= c `
by Def4;
A2:
a ` = c `
by Def4;
hence
( a = 0 implies a ` = 3 )
; ( ( a = 3 implies a ` = 0 ) & ( a = 1 implies a ` = 3 \ 1 ) & ( a = 3 \ 1 implies a ` = 1 ) & ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
A3:
( a ` = {} or a ` = {0} or a ` = {1} or a ` = {2} or a ` = {0,1} or a ` = {1,2} or a ` = {0,2} or a ` = {0,1,2} )
by A2, YELLOW11:1, ZFMISC_1:118;
thus
( a = 3 implies a ` = 0 )
( ( a = 1 implies a ` = 3 \ 1 ) & ( a = 3 \ 1 implies a ` = 1 ) & ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )proof
assume A4:
a = 3
;
a ` = 0
then
1
in c
by ENUMSET1:def 1, YELLOW11:1;
then A5:
not 1
in a `
by A1, XBOOLE_0:def 5;
2
in c
by A4, ENUMSET1:def 1, YELLOW11:1;
then A6:
not 2
in a `
by A1, XBOOLE_0:def 5;
not
0 in c `
by A4, XBOOLE_0:def 5;
then
not
0 in a `
by Def4;
hence
a ` = 0
by A3, A5, A6, ENUMSET1:def 1, TARSKI:def 1, TARSKI:def 2;
verum
end;
thus
( a = 1 implies a ` = 3 \ 1 )
by A2; ( ( a = 3 \ 1 implies a ` = 1 ) & ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
A7:
0 in 3
by ENUMSET1:def 1, YELLOW11:1;
thus
( a = 3 \ 1 implies a ` = 1 )
( ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )proof
assume A8:
a = 3
\ 1
;
a ` = 1
then
1
in c
by TARSKI:def 2, YELLOW11:3;
then A9:
not 1
in a `
by A1, XBOOLE_0:def 5;
2
in c
by A8, TARSKI:def 2, YELLOW11:3;
then A10:
not 2
in a `
by A1, XBOOLE_0:def 5;
not
0 in c
by A8, TARSKI:def 2, YELLOW11:3;
hence
a ` = 1
by A7, A2, A3, A9, A10, CARD_1:49, ENUMSET1:def 1, TARSKI:def 1, TARSKI:def 2, XBOOLE_0:def 5;
verum
end;
thus
( a = 2 implies a ` = 3 \ 2 )
by A2; ( a = 3 \ 2 implies a ` = 2 )
assume A11:
a = 3 \ 2
; a ` = 2
then
2 in c
by TARSKI:def 1, YELLOW11:4;
then A12:
not 2 in a `
by A1, XBOOLE_0:def 5;
( 1 in 3 & not 1 in c )
by A11, ENUMSET1:def 1, TARSKI:def 1, YELLOW11:1, YELLOW11:4;
then A13:
1 in a `
by A2, XBOOLE_0:def 5;
not 0 in c
by A11, TARSKI:def 1, YELLOW11:4;
then
0 in a `
by A7, A2, XBOOLE_0:def 5;
hence
a ` = 2
by A3, A12, A13, CARD_1:50, ENUMSET1:def 1, TARSKI:def 1, TARSKI:def 2; verum