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