:: deftheorem defines out GTARSKI5:def 6 :
for S being non empty TarskiGeometryStruct
for a, b, p, q being POINT of S holds
( p,q out a,b iff ( p <> q & Line (p,q) out a,b ) );