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