let UN be non trivial Universe; :: thesis: for n being Nat holds REAL n in UN
let n be Nat; :: thesis: REAL n in UN
( REAL is Element of UN & n -tuples_on REAL = REAL n ) by EUCLID:def 1, Th53;
hence REAL n in UN by Th58; :: thesis: verum