:: deftheorem defines are_concurrent MENELAUS:def 1 :
for X, Y, Z being Subset of (TOP-REAL 2) holds
( X,Y,Z are_concurrent iff ( ( X is_parallel_to Y & Y is_parallel_to Z & Z is_parallel_to X ) or ex A being Point of (TOP-REAL 2) st
( A in X & A in Y & A in Z ) ) );