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
space3 (A,r) = { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) }
let r be POINT of S; :: thesis: for A being Subset of S st A is_plane & not r in A holds
space3 (A,r) = { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) }
let A be Subset of S; :: thesis: ( A is_plane & not r in A implies space3 (A,r) = { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) } )
assume that
A1: A is_plane and
A2: not r in A ; :: thesis: space3 (A,r) = { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) }
consider r9 being POINT of S such that
A3: between2 r,A,r9 and
A4: space3 (A,r) = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) by A1, A2, Def20;
set P = { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) } ;
A5: space3 (A,r) c= { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in space3 (A,r) or x in { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) } )
assume x in space3 (A,r) ; :: thesis: x in { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) }
then ( x in (half-space3 (A,r)) \/ A or x in half-space3 (A,r9) ) by A4, XBOOLE_0:def 3;

per cases then ( x in half-space3 (A,r) or x in A or x in half-space3 (A,r9) ) by XBOOLE_0:def 3;

suppose x in half-space3 (A,r) ; :: thesis: x in { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) }

then x in { x where x is POINT of S : A out2 x,r } by A1, A2, Def18;
then ex y being POINT of S st
( x = y & A out2 y,r ) ;
hence x in { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) } ; :: thesis: verum

end;

suppose x in A ; :: thesis: x in { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) }

hence x in { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) } ; :: thesis: verum

end;

suppose A6: x in half-space3 (A,r9) ; :: thesis: x in { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) }

then reconsider y = x as POINT of S ;
x in { x where x is POINT of S : A out2 x,r9 } by A3, A6, Def18;
then consider z being POINT of S such that
A7: x = z and
A8: A out2 z,r9 ;
( between2 r9,A,r & A out2 r9,y ) by A7, A8, A3, GTARSKI3:14;
then between2 y,A,r by Th74;
then between2 r,A,y by GTARSKI3:14;
hence x in { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) } ; :: thesis: verum

end;

end;

end;

{ x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) } c= space3 (A,r)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) } or x in space3 (A,r) )
assume x in { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) } ; :: thesis: x in space3 (A,r)
then consider y being POINT of S such that
A9: y = x and
A10: ( A out2 y,r or y in A or between2 r,A,y ) ;

per cases ( A out2 y,r or y in A or between2 r,A,y ) by A10;

suppose A out2 y,r ; :: thesis: x in space3 (A,r)

then y in { x where x is POINT of S : A out2 x,r } ;
then x in half-space3 (A,r) by A9, A1, A2, Def18;
then x in (half-space3 (A,r)) \/ A by XBOOLE_0:def 3;
hence x in space3 (A,r) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose y in A ; :: thesis: x in space3 (A,r)

then x in (half-space3 (A,r)) \/ A by A9, XBOOLE_0:def 3;
hence x in space3 (A,r) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose between2 r,A,y ; :: thesis: x in space3 (A,r)

then ( between2 y,A,r & between2 r9,A,r ) by A3, GTARSKI3:14;
then A out2 y,r9 ;
then x in { x where x is POINT of S : A out2 x,r9 } by A9;
then x in half-space3 (A,r9) by A3, Def18;
then x in A \/ (half-space3 (A,r9)) by XBOOLE_0:def 3;
then x in (half-space3 (A,r)) \/ (A \/ (half-space3 (A,r9))) by XBOOLE_0:def 3;
hence x in space3 (A,r) by A4, XBOOLE_1:4; :: thesis: verum

end;

end;

end;

hence space3 (A,r) = { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) } by A5; :: thesis: verum