let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for r being POINT of S
for A being Subset of S st A is_plane & not r in A holds
half-space3 (A,r) c= space3 (A,r)
let r be POINT of S; :: thesis: for A being Subset of S st A is_plane & not r in A holds
half-space3 (A,r) c= space3 (A,r)
let A be Subset of S; :: thesis: ( A is_plane & not r in A implies half-space3 (A,r) c= space3 (A,r) )
assume ( A is_plane & not r in A ) ; :: thesis: half-space3 (A,r) c= space3 (A,r)
then consider r9 being POINT of S such that
between2 r,A,r9 and
A1: space3 (A,r) = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) by Def20;
( half-space3 (A,r) c= (half-space3 (A,r)) \/ A & (half-space3 (A,r)) \/ A c= ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) ) by XBOOLE_1:7;
hence half-space3 (A,r) c= space3 (A,r) by A1; :: thesis: verum