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 that
A1: A // C and
A2: p in A and
A3: p in C ; :: thesis: 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; :: thesis: for p being Element of AS st A // C & p in A & p in C holds
A c= C
let p be Element of AS; :: thesis: ( 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 ; :: thesis: A c= C
A8: C is being_line by A5, Th50;
A9: A is being_line by A5, Th50;

now

let x be set ; :: thesis: ( x in A implies x in C )
assume A10: x in A ; :: thesis: x in C
then reconsider x9 = x as Element of AS ;

now

consider q being Element of AS such that
A11: p <> q and
A12: q in C by A8, Th32;
assume A13: x9 <> p ; :: thesis: x in C
then A = Line (p,x9) by A6, A9, A10, Lm6;
then p,x9 // C by A5, A13, Th43, Th57;
then p,x9 // p,q by A7, A8, A11, A12, Th41;
then p,q // p,x9 by Th13;
then A14: LIN p,q,x9 by Def1;
C = Line (p,q) by A7, A8, A11, A12, Lm6;
hence x in C by A14, Def2; :: thesis: verum

end;

hence x in C by A7; :: thesis: verum

end;

hence A c= C by TARSKI:def 3; :: thesis: 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; :: thesis: verum