for AS being AffinSpace
for p being Element of AS
for A, C, D being Subset of AS st A // C & A // D & p in C & p in D holds
C = D by Lm7, Th44;