theorem Th11: :: SPPOL_2:11

L~ (<*> the carrier of (TOP-REAL 2)) = {} by TOPREAL1:22;