let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; for a being POINT of S holds a,a,a,a are_coplanar
let a be POINT of S; a,a,a,a are_coplanar
consider b being POINT of S such that
between a,a,b
and
A1:
a <> b
by GTARSKI3:36;
consider c being POINT of S such that
A2:
not Collinear a,b,c
by A1, GTARSKI3:92;
consider E being Subset of S such that
Plane (a,b,c) = E
and
A3:
E is_plane
and
A4:
a in E
and
b in E
and
c in E
by A2, Th49;
take
E
; GTARSKI5:def 15 ( E is_plane & a in E & a in E & a in E & a in E )
thus
( E is_plane & a in E & a in E & a in E & a in E )
by A3, A4; verum