let n be Element of NAT ; :: thesis: G0 . n is Interval
G0 . n in {REAL } by Lm1, FUNCT_2:6;
hence G0 . n is Interval by TARSKI:def 1; :: thesis: verum