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;

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

hence
a,b // C
; :: thesis: verumconsider 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;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