per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: IFEQ x,y,a,b is natural

hence IFEQ x,y,a,b is natural by FUNCOP_1:def 8; :: thesis: verum

end;

suppose x <> y ; :: thesis: IFEQ x,y,a,b is natural

hence IFEQ x,y,a,b is natural by FUNCOP_1:def 8; :: thesis: verum

end;

end;