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