let AS be AffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( A // C & p in A & p in C implies A = C )
assume A1:
( A // C & p in A & p in C )
; :: thesis: A = C
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;
:: thesis: for p being Element of AS st A // C & p in A & p in C holds
A c= Clet p be
Element of
AS;
:: thesis: ( A // C & p in A & p in C implies A c= C )
assume A2:
(
A // C &
p in A &
p in C )
;
:: thesis: A c= C
then A3:
(
A is
being_line &
C is
being_line )
by Th50;
now let x be
set ;
:: thesis: ( x in A implies x in C )assume A4:
x in A
;
:: thesis: x in Cthen reconsider x' =
x as
Element of
AS ;
now assume A5:
x' <> p
;
:: thesis: x in Cthen
A = Line p,
x'
by A2, A3, A4, Lm6;
then A6:
p,
x' // C
by A2, A5, Th43, Th57;
consider q being
Element of
AS such that A7:
(
p <> q &
q in C )
by A3, Th32;
A8:
C = Line p,
q
by A2, A3, A7, Lm6;
p,
x' // p,
q
by A2, A3, A6, A7, Th41;
then
p,
q // p,
x'
by Th13;
then
LIN p,
q,
x'
by Def1;
hence
x in C
by A8, Def2;
:: thesis: verum end; hence
x in C
by A2;
:: thesis: verum end;
hence
A c= C
by TARSKI:def 3;
:: thesis: verum
end;
then
( A c= C & C c= A )
by A1;
hence
A = C
by XBOOLE_0:def 10; :: thesis: verum