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