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
( A c= space3 (A,r) & r in 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
( A c= space3 (A,r) & r in space3 (A,r) )
let A be Subset of S; :: thesis: ( A is_plane & not r in A implies ( A c= space3 (A,r) & r in space3 (A,r) ) )
assume that
A1: A is_plane and
A2: not r in A ; :: thesis: ( A c= space3 (A,r) & r in space3 (A,r) )
ex r9 being POINT of S st
( between2 r,A,r9 & space3 (A,r) = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) ) by A1, A2, Def20;
then A3: ( A c= (half-space3 (A,r)) \/ A & (half-space3 (A,r)) \/ A c= space3 (A,r) ) by XBOOLE_1:7;
( r in half-space3 (A,r) & half-space3 (A,r) c= space3 (A,r) ) by A1, A2, Th80, Th84;
hence ( A c= space3 (A,r) & r in space3 (A,r) ) by A3; :: thesis: verum