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

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

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

end;

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

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

end;

end;