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