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