let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; for r, s being POINT of S
for A being Subset of S st A is_line & not r in A & s in Plane (A,r) & not s in A holds
Plane (A,r) = Plane (A,s)
let r, s be POINT of S; for A being Subset of S st A is_line & not r in A & s in Plane (A,r) & not s in A holds
Plane (A,r) = Plane (A,s)
let A be Subset of S; ( A is_line & not r in A & s in Plane (A,r) & not s in A implies Plane (A,r) = Plane (A,s) )
assume that
A1:
A is_line
and
A2:
not r in A
and
A3:
s in Plane (A,r)
and
A4:
not s in A
; Plane (A,r) = Plane (A,s)
consider r9 being POINT of S such that
A5:
between r,A,r9
and
A6:
Plane (A,r) = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9))
by A1, A2, Def10;
consider s9 being POINT of S such that
A7:
between s,A,s9
and
A8:
Plane (A,s) = ((half-plane (A,s)) \/ A) \/ (half-plane (A,s9))
by A1, A4, Def10;
( s in ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) & s in (half-plane (A,r)) \/ (A \/ (half-plane (A,r9))) )
by A3, A6, XBOOLE_1:4;
then
( ( s in (half-plane (A,r)) \/ A or s in half-plane (A,r9) ) & ( s in half-plane (A,r) or s in A \/ (half-plane (A,r9)) ) )
by XBOOLE_0:def 3;
per cases then
( s in half-plane (A,r) or s in half-plane (A,r9) )
by A4, XBOOLE_0:def 3;
suppose A9:
s in half-plane (
A,
r)
;
Plane (A,r) = Plane (A,s)
ex
x being
POINT of
S st
(
s = x &
A out x,
r )
by A9;
then
between r,
A,
s9
by A7, Th14;
then T1:
between s9,
A,
r
by GTARSKI3:14;
between r9,
A,
r
by A5, GTARSKI3:14;
then
A out s9,
r9
by T1;
then
s9 in half-plane (
A,
r9)
;
then
half-plane (
A,
r9)
= half-plane (
A,
s9)
by A5, A7, Th23;
hence
Plane (
A,
r)
= Plane (
A,
s)
by A9, A1, A2, A4, Th23, A6, A8;
verum suppose A10:
s in half-plane (
A,
r9)
;
Plane (A,r) = Plane (A,s)then A11:
half-plane (
A,
r9)
= half-plane (
A,
s)
by A4, A5, Th23;
consider y being
POINT of
S such that A12:
s = y
and A13:
A out y,
r9
by A10;
half-plane (
A,
r)
= half-plane (
A,
s9)
proof
T1:
between s9,
A,
s
by A7, GTARSKI3:14;
(
between r9,
A,
r &
A out r9,
y )
by A13, A5, GTARSKI3:14;
then
between y,
A,
r
by Th14;
then
between r,
A,
s
by A12, GTARSKI3:14;
then
A out s9,
r
by T1;
then
s9 in half-plane (
A,
r)
;
hence
half-plane (
A,
r)
= half-plane (
A,
s9)
by A5, A7, Th23;
verum
end; hence
Plane (
A,
r)
= Plane (
A,
s)
by A11, A6, A8, XBOOLE_1:4;
verum end;