the carrier of (ConvergenceSpace C) = the carrier of S by Def27;
hence not the carrier of (ConvergenceSpace C) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum