let a be rational number ; :: thesis: for b being real irrational number holds b - a is irrational
let b be real irrational number ; :: thesis: b - a is irrational
b + (- a) is irrational by Th38;
hence b - a is irrational ; :: thesis: verum