let AS be AffinSpace; 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; 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; 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; verum