theorem THSS2: :: GTARSKI2:32

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