let UN be non trivial Universe; :: thesis: REAL is Element of UN
reconsider n = NAT as Element of UN by Def6;
reconsider n1 = [:n,n:] \/ n as Element of UN ;
reconsider n2 = n1 \/ (bool n1) as Element of UN ;
REAL c= n2 \/ [:n,n2:] by Th52;
hence REAL is Element of UN by Th13; :: thesis: verum