:: deftheorem defines are_in_this_order_on JORDAN17:def 1 :
for P being Subset of (TOP-REAL 2)
for a, b, c, d being Point of (TOP-REAL 2) holds
( a,b,c,d are_in_this_order_on P iff ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) );