theorem Satz6p28Lem01: :: GTARSKI3:93

for S being satisfying_Tarski-model TarskiGeometryStruct
for p, a, b being POINT of S st p out a,b & p,a <= p,b holds
between p,a,b by Satz6p13;