let AS be AffinSpace; :: thesis: for a, b being Element of AS
for A, C being Subset of AS st a in A & b in A & A // C holds
a,b // C
let a, b be Element of AS; :: thesis: for A, C being Subset of AS st a in A & b in A & A // C holds
a,b // C
let A, C be Subset of AS; :: thesis: ( a in A & b in A & A // C implies a,b // C )
assume that
A1: a in A and
A2: b in A and
A3: A // C ; :: thesis: a,b // C
A4: C is being_line by A3, Th35;

now :: thesis: a,b // C

consider p, q being Element of AS such that
A5: p in C and
A6: q in C and
A7: p <> q by A4, Th18;
A8: C = Line (p,q) by A4, A5, A6, A7, Lm6;
a,b // p,q by A1, A2, A3, A5, A6, Th38;
hence a,b // C by A7, A8; :: thesis: verum

end;

hence a,b // C ; :: thesis: verum