reconsider a = the irrational Real as Element of F_Real by XREAL_0:def 1;
take a ; :: thesis: a is irrational
thus a is irrational ; :: thesis: verum