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;