theorem Th69:
for
S being non
empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct for
a,
b,
c being
POINT of
S st not
Collinear a,
b,
c holds
(
Plane (
a,
b,
c)
is_plane &
a in Plane (
a,
b,
c) &
b in Plane (
a,
b,
c) &
c in Plane (
a,
b,
c) & ( for
u,
v being
POINT of
S st
u in Plane (
a,
b,
c) &
v in Plane (
a,
b,
c) &
u <> v holds
Line (
u,
v)
c= Plane (
a,
b,
c) ) )