let a, x be Element of Benzene; :: thesis: ( a = 0 implies a "/\" x = a )
assume a = 0 ; :: thesis: a "/\" x = a
then a c= x ;
then a [= x by Th24;
hence a "/\" x = a by LATTICES:4; :: thesis: verum