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 by XBOOLE_1:2;
then a [= x by Th24;
hence a "\/" x = x by LATTICES:def 3; :: thesis: verum