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 ` = or a ` = {1} or a ` = {2} or a ` = {0,1} or a ` = {1,2} or a ` = {0,2} or a ` = {0,1,2} ) by ;
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
assume A4: a = 3 ; :: thesis: a ` = 0
then 1 in c by ;
then A5: not 1 in a ` by ;
2 in c by ;
then A6: not 2 in a ` by ;
not 0 in c ` by ;
then not 0 in a ` by Def4;
hence a ` = 0 by ; :: thesis: verum
end;
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 ) )
A7: 0 in 3 by ;
thus ( a = 3 \ 1 implies a ` = 1 ) :: thesis: ( ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
proof
assume A8: a = 3 \ 1 ; :: thesis: a ` = 1
then 1 in c by ;
then A9: not 1 in a ` by ;
2 in c by ;
then A10: not 2 in a ` by ;
not 0 in c by ;
hence a ` = 1 by ; :: thesis: verum
end;
thus ( a = 2 implies a ` = 3 \ 2 ) by A2; :: thesis: ( a = 3 \ 2 implies a ` = 2 )
assume A11: a = 3 \ 2 ; :: thesis: a ` = 2
then 2 in c by ;
then A12: not 2 in a ` by ;
( 1 in 3 & not 1 in c ) by ;
then A13: 1 in a ` by ;
not 0 in c by ;
then 0 in a ` by ;
hence a ` = 2 by ; :: thesis: verum