let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p1,p2,p3 are_mutually_different & angle p1,p2,p3 > PI implies ( angle p2,p3,p1 > PI & angle p3,p1,p2 > PI ) )
assume A1: p1,p2,p3 are_mutually_different ; :: 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_different 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_different by A2, A4, ZFMISC_1:def 5;
hence angle p3,p1,p2 > PI by A3, Th23; :: thesis: verum