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