let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for p, r being POINT of S
for A, A9 being Subset of S st A,A9 Is p & r in A9 & r <> p holds
A9 c= Plane (A,r)
let p, r be POINT of S; :: thesis: for A, A9 being Subset of S st A,A9 Is p & r in A9 & r <> p holds
A9 c= Plane (A,r)
let A, A9 be Subset of S; :: thesis: ( A,A9 Is p & r in A9 & r <> p implies A9 c= Plane (A,r) )
assume that
A1: A,A9 Is p and
A2: r in A9 and
A3: r <> p ; :: thesis: A9 c= Plane (A,r)
A4: A9 = Line (p,r) by A1, A2, A3, GTARSKI3:87;
A5: not r in A by A1, A2, A3, GTARSKI3:89;
then A6: Plane (A,r) = { x where x is POINT of S : ( A out x,r or x in A or between r,A,x ) } by A1, Th32;

now :: thesis: for x being object st x in A9 holds
x in Plane (A,r)

let x be object ; :: thesis: ( x in A9 implies b₁ in Plane (A,r) )
assume A7: x in A9 ; :: thesis: b₁ in Plane (A,r)
then consider y being POINT of S such that
A8: x = y ;
consider z being POINT of S such that
A9: y = z and
A10: Collinear p,r,z by A4, A7, A8;

per cases ( x = p or x <> p ) ;

suppose A11: x = p ; :: thesis: b₁ in Plane (A,r)

A c= Plane (A,r) by A1, A5, Th31;
hence x in Plane (A,r) by A11, A1; :: thesis: verum

end;

suppose A12: x <> p ; :: thesis: b₁ in Plane (A,r)

per cases ( between r,p,z or not between r,p,z ) ;

suppose between r,p,z ; :: thesis: b₁ in Plane (A,r)

then between r,A,z by A1, A2, A3, A9, A8, A7, A12, GTARSKI3:89;
hence x in Plane (A,r) by A8, A9, A6; :: thesis: verum

end;

suppose A13: not between r,p,z ; :: thesis: b₁ in Plane (A,r)

Collinear r,p,z by A10, GTARSKI3:14;
then A14: p out r,z by A13, GTARSKI3:73;
A15: not reflection (p,r) in A

proof

assume A16: reflection (p,r) in A ; :: thesis: contradiction
( A is_line & A9 is_line & reflection (p,r) in A9 ) by A1, A2, Th36;
then Middle r,p,p by A1, A16, GTARSKI3:89, GTARSKI3:def 13;
hence contradiction by A3, GTARSKI1:def 7; :: thesis: verum

end;

between z,p, reflection (p,r)

proof

per cases ( between p,r,z or between p,z,r ) by A14;

suppose between p,r,z ; :: thesis: between z,p, reflection (p,r)

then A17: between z,r,p by GTARSKI3:14;
Middle r,p, reflection (p,r) by GTARSKI3:def 13;
hence between z,p, reflection (p,r) by A3, A17, GTARSKI3:19; :: thesis: verum

end;

suppose between p,z,r ; :: thesis: between z,p, reflection (p,r)

then A18: between r,z,p by GTARSKI3:14;
Middle r,p, reflection (p,r) by GTARSKI3:def 13;
hence between z,p, reflection (p,r) by A18, GTARSKI3:18; :: thesis: verum

end;

end;

end;

then U1: between z,A, reflection (p,r) by A9, A8, A7, A12, GTARSKI3:89, A15, A1;
Middle r,p, reflection (p,r) by GTARSKI3:def 13;
then between r,A, reflection (p,r) by A1, A2, A3, GTARSKI3:89, A15;
then A out z,r by U1;
hence x in Plane (A,r) by A9, A8, A6; :: thesis: verum

end;

end;

end;

end;

end;

hence A9 c= Plane (A,r) ; :: thesis: verum