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