set B = Benzene ;

let a be Element of Benzene; :: thesis: ( ( 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 ) ; :: thesis: ( ( 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 ) :: thesis: ( ( a = 1 implies a ` = 3 \ 1 ) & ( 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 ) :: thesis: ( ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )

assume A11: a = 3 \ 2 ; :: thesis: 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; :: thesis: verum

let a be Element of Benzene; :: thesis: ( ( 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 ) ; :: thesis: ( ( 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 ) :: thesis: ( ( 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

thus
( a = 1 implies a ` = 3 \ 1 )
by A2; :: thesis: ( ( a = 3 \ 1 implies a ` = 1 ) & ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
assume A4:
a = 3
; :: thesis: 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; :: thesis: verum

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

A7: 0 in 3 by ENUMSET1:def 1, YELLOW11:1;

thus ( a = 3 \ 1 implies a ` = 1 ) :: thesis: ( ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )

proof

thus
( a = 2 implies a ` = 3 \ 2 )
by A2; :: thesis: ( a = 3 \ 2 implies a ` = 2 )
assume A8:
a = 3 \ 1
; :: thesis: 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; :: thesis: verum

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

assume A11: a = 3 \ 2 ; :: thesis: 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; :: thesis: verum