set A = the Simple_closed_curve;
take the Simple_closed_curve ; :: thesis: not the Simple_closed_curve is empty
thus not the Simple_closed_curve is empty ; :: thesis: verum