let P1, P2 be Subset of S; ( ex r being POINT of S st
( not r in A & r in A9 & P1 = Plane (A,r) ) & ex r being POINT of S st
( not r in A & r in A9 & P2 = Plane (A,r) ) implies P1 = P2 )
assume that
A7:
ex r being POINT of S st
( not r in A & r in A9 & P1 = Plane (A,r) )
and
A8:
ex r being POINT of S st
( not r in A & r in A9 & P2 = Plane (A,r) )
; P1 = P2
consider r being POINT of S such that
A9:
not r in A
and
A10:
r in A9
and
A11:
P1 = Plane (A,r)
by A7;
consider s being POINT of S such that
A12:
not s in A
and
A13:
s in A9
and
A14:
P2 = Plane (A,s)
by A8;
consider p being POINT of S such that
A15:
p in A /\ A9
by A4;
( p in A9 & p in A )
by A15, XBOOLE_0:def 4;
then
A9 c= Plane (A,r)
by A9, A10, Th37, A1, A2, GTARSKI4:def 7;
hence
P1 = P2
by A13, A1, A9, A12, A11, A14, Th34; verum