theorem Th45:
for
S being non
empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct for
a,
b,
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) & not
b in Line (
p,
q) &
Line (
p,
q)
<> Line (
a,
b) holds
(
Line (
a,
b)
c= E & ex
c being
POINT of
S st
( not
Collinear a,
b,
c &
E = Plane (
a,
b,
c) ) )