let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a being POINT of S
for A being Subset of S st A is_plane & not a in A holds
A out2 a,a
let a be POINT of S; :: thesis: for A being Subset of S st A is_plane & not a in A holds
A out2 a,a
let A be Subset of S; :: thesis: ( A is_plane & not a in A implies A out2 a,a )
assume ( A is_plane & not a in A ) ; :: thesis: A out2 a,a
then ex c being POINT of S st between2 a,A,c by Th76;
hence A out2 a,a ; :: thesis: verum