let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies not A in Line (B,C) )
assume A1: A,B,C is_a_triangle ; :: thesis: not A in Line (B,C)
then A2: A,B,C are_mutually_distinct by EUCLID_6:20;
assume A in Line (B,C) ; :: thesis: contradiction
hence contradiction by A1, A2, MENELAUS:13; :: thesis: verum