let AS be AffinSpace; for p being Element of AS
for A, C being Subset of AS st A // C & p in A & p in C holds
A = C
let p be Element of AS; for A, C being Subset of AS st A // C & p in A & p in C holds
A = C
let A, C be Subset of AS; ( A // C & p in A & p in C implies A = C )
assume that
A1:
A // C
and
A2:
p in A
and
A3:
p in C
; A = C
A4:
for A, C being Subset of AS
for p being Element of AS st A // C & p in A & p in C holds
A c= C
proof
let A,
C be
Subset of
AS;
for p being Element of AS st A // C & p in A & p in C holds
A c= Clet p be
Element of
AS;
( A // C & p in A & p in C implies A c= C )
assume that A5:
A // C
and A6:
p in A
and A7:
p in C
;
A c= C
A8:
C is
being_line
by A5, Th35;
A9:
A is
being_line
by A5;
let x be
object ;
TARSKI:def 3 ( not x in A or x in C )
assume A10:
x in A
;
x in C
then reconsider x9 =
x as
Element of
AS ;
now ( x9 <> p implies x in C )consider q being
Element of
AS such that A11:
p <> q
and A12:
q in C
by A8, Th19;
assume A13:
x9 <> p
;
x in Cthen
A = Line (
p,
x9)
by A6, A9, A10, Lm6;
then
p,
x9 // C
by A5, A13, Th28, Th42;
then
p,
x9 // p,
q
by A7, A8, A11, A12, Th26;
then
p,
q // p,
x9
by Th3;
then A14:
LIN p,
q,
x9
;
C = Line (
p,
q)
by A7, A8, A11, A12, Lm6;
hence
x in C
by A14, Def2;
verum end;
hence
x in C
by A7;
verum
end;
then A15:
C c= A
by A1, A2, A3;
A c= C
by A1, A2, A3, A4;
hence
A = C
by A15, XBOOLE_0:def 10; verum