let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; for a being POINT of S
for A being Subset of S st A is_plane & not a in A holds
a in half-space3 (A,a)
let a be POINT of S; for A being Subset of S st A is_plane & not a in A holds
a in half-space3 (A,a)
let A be Subset of S; ( A is_plane & not a in A implies a in half-space3 (A,a) )
assume that
A1:
A is_plane
and
A2:
not a in A
; a in half-space3 (A,a)
A3:
half-space3 (A,a) = { x where x is POINT of S : A out2 x,a }
by A1, A2, Def18;
A out2 a,a
by Th77, A1, A2;
hence
a in half-space3 (A,a)
by A3; verum