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;