theorem THSS: :: GTARSKI2:31

for a, b, c being Element of (OASpace (TOP-REAL 2)) holds
( Mid a,b,c iff ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) )