theorem Prelim07:
for
S being non
empty satisfying_Tarski-model TarskiGeometryStruct for
p,
q,
r being
POINT of
S st
p <> q &
p <> r & (
Collinear p,
q,
r or
Collinear q,
r,
p or
Collinear r,
p,
q or
Collinear p,
r,
q or
Collinear q,
p,
r or
Collinear r,
q,
p ) holds
(
Line (
p,
q)
= Line (
p,
r) &
Line (
p,
q)
= Line (
r,
p) &
Line (
q,
p)
= Line (
p,
r) &
Line (
q,
p)
= Line (
r,
p) )