let D be Simple_closed_curve; :: thesis: not D is trivial
ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in D & p2 in D ) by TOPREAL2:5;
hence not D is trivial ; :: thesis: verum