let AS be AffinSpace; :: thesis: for a being Element of AS
for A being Subset of AS st A is being_line holds
ex C being Subset of AS st
( a in C & A // C )
let a be Element of AS; :: thesis: for A being Subset of AS st A is being_line holds
ex C being Subset of AS st
( a in C & A // C )
let A be Subset of AS; :: thesis: ( A is being_line implies ex C being Subset of AS st
( a in C & A // C ) )
assume A is being_line ; :: thesis: ex C being Subset of AS st
( a in C & A // C )
then 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:47;
set C = Line a,b;
A5: a in Line a,b by Th26;
A // Line a,b by A1, A2, A3, A4, Th51;
hence ex C being Subset of AS st
( a in C & A // C ) by A5; :: thesis: verum