let x be Element of F; :: thesis: x is Subset of REAL
thus x is Subset of REAL ; :: thesis: verum