consider C being non empty convex Subset of ;
take C ; :: thesis: ( not C is empty & C is convex )
thus ( not C is empty & C is convex ) ; :: thesis: verum