let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p1,p2,p3 are_mutually_distinct & angle (p1,p2,p3) > PI implies ( angle (p2,p3,p1) > PI & angle (p3,p1,p2) > PI ) )
assume A1: p1,p2,p3 are_mutually_distinct ; :: thesis: ( not angle (p1,p2,p3) > PI or ( angle (p2,p3,p1) > PI & angle (p3,p1,p2) > PI ) )
then A2: ( p1 <> p2 & p1 <> p3 ) by ZFMISC_1:def 5;
assume A3: angle (p1,p2,p3) > PI ; :: thesis: ( angle (p2,p3,p1) > PI & angle (p3,p1,p2) > PI )
A4: p2 <> p3 by A1, ZFMISC_1:def 5;
then p2,p3,p1 are_mutually_distinct by A2, ZFMISC_1:def 5;
hence angle (p2,p3,p1) > PI by A3, Th23; :: thesis: angle (p3,p1,p2) > PI
p3,p1,p2 are_mutually_distinct by A2, A4, ZFMISC_1:def 5;
hence angle (p3,p1,p2) > PI by A3, Th23; :: thesis: verum