( x = y or x <> y ) ;
hence IFEQ x,y,a,b is Element of D by Def8; :: thesis: verum