consider A being Simple_closed_curve;
take A ; :: thesis: not A is empty
thus not A is empty ; :: thesis: verum