let a, b be Element of Benzene; :: thesis: ( a [= b iff a c= b )
reconsider x = a, y = b as Element of B_6 by Th9, YELLOW_1:1;

hereby :: thesis: ( a c= b implies a [= b )

assume a [= b ; :: thesis: a c= b
then x <= y by Th13;
hence a c= b by YELLOW_1:3; :: thesis: verum

end;

assume a c= b ; :: thesis: a [= b
then x <= y by YELLOW_1:3;
hence a [= b by Th13; :: thesis: verum