( r -' s = r - s or r -' s = 0 ) by Def2;
hence r -' s is real ; :: thesis: verum