let x be set ; :: according to FUNCT_1:def 13 :: thesis: ( not x in the carrier of (TOP-REAL n) or x is set )
thus ( not x in the carrier of (TOP-REAL n) or x is set ) by EUCLID:23; :: thesis: verum