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

proof

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

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

suppose x in half-plane (A,r) ; :: thesis: x in { x where x is POINT of S : ( A out x,r or x in A or between r,A,x ) }

then ex y being POINT of S st
( x = y & A out y,r ) ;
hence x in { x where x is POINT of S : ( A out x,r or x in A or between r,A,x ) } ; :: thesis: verum

end;

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

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

end;

suppose A6: x in half-plane (A,r9) ; :: thesis: x in { x where x is POINT of S : ( A out x,r or x in A or between r,A,x ) }

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

end;

end;

end;

{ x where x is POINT of S : ( A out x,r or x in A or between r,A,x ) } c= Plane (A,r)

proof

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

per cases ( A out y,r or y in A or between r,A,y ) by A10;

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

then y in { x where x is POINT of S : A out x,r } ;
then x in (half-plane (A,r)) \/ A by A9, XBOOLE_0:def 3;
hence x in Plane (A,r) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

hence Plane (A,r) = { x where x is POINT of S : ( A out x,r or x in A or between r,A,x ) } by A5; :: thesis: verum