theorem Th44:
for
S being non
empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct for
a,
b,
c,
p,
q,
r being
POINT of
S for
E being
Subset of
S st
a in E &
b in E &
a <> b & not
Collinear p,
q,
r &
E = Plane (
p,
q,
r) &
c in Line (
p,
q) & not
c in Line (
a,
b) & not
b in Line (
p,
q) holds
(
Line (
a,
b)
c= E & ex
c being
POINT of
S st
( not
Collinear a,
b,
c &
E = Plane (
a,
b,
c) ) )