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;

assume a c= b ; :: thesis: a [= b

then x <= y by YELLOW_1:3;

hence a [= b by Th13; :: thesis: verum

reconsider x = a, y = b as Element of B_6 by Th9, YELLOW_1:1;

assume a c= b ; :: thesis: a [= b

then x <= y by YELLOW_1:3;

hence a [= b by Th13; :: thesis: verum