let AS be AffinSpace; :: thesis: for a being Element of AS

for A being being_line Subset of AS ex C being Subset of AS st

( a in C & A // C )

let a be Element of AS; :: thesis: for A being being_line Subset of AS ex C being Subset of AS st

( a in C & A // C )

let A be being_line Subset of AS; :: thesis: ex C being Subset of AS st

( a in C & A // C )

consider p, q being Element of AS such that

A1: p <> q and

A2: A = Line (p,q) by Def3;

consider b being Element of AS such that

A3: p,q // a,b and

A4: a <> b by DIRAF:40;

set C = Line (a,b);

A5: a in Line (a,b) by Th14;

A // Line (a,b) by A1, A2, A3, A4, Th36;

hence ex C being Subset of AS st

( a in C & A // C ) by A5; :: thesis: verum

for A being being_line Subset of AS ex C being Subset of AS st

( a in C & A // C )

let a be Element of AS; :: thesis: for A being being_line Subset of AS ex C being Subset of AS st

( a in C & A // C )

let A be being_line Subset of AS; :: thesis: ex C being Subset of AS st

( a in C & A // C )

consider p, q being Element of AS such that

A1: p <> q and

A2: A = Line (p,q) by Def3;

consider b being Element of AS such that

A3: p,q // a,b and

A4: a <> b by DIRAF:40;

set C = Line (a,b);

A5: a in Line (a,b) by Th14;

A // Line (a,b) by A1, A2, A3, A4, Th36;

hence ex C being Subset of AS st

( a in C & A // C ) by A5; :: thesis: verum