set C = the non empty convex Subset of (TOP-REAL 2);
take the non empty convex Subset of (TOP-REAL 2) ; :: thesis: ( not the non empty convex Subset of (TOP-REAL 2) is empty & the non empty convex Subset of (TOP-REAL 2) is convex )
thus ( not the non empty convex Subset of (TOP-REAL 2) is empty & the non empty convex Subset of (TOP-REAL 2) is convex ) ; :: thesis: verum