let AS be AffinSpace; the carrier of AS misses Dir_of_Lines AS
assume
not the carrier of AS misses Dir_of_Lines AS
; contradiction
then consider x being object such that
A1:
x in the carrier of AS
and
A2:
x in Dir_of_Lines AS
by XBOOLE_0:3;
reconsider a = x as Element of AS by A1;
consider X being Subset of AS such that
A3:
x = LDir X
and
A4:
X is being_line
by A2, Th14;
set A = a * X;
A5:
a * X is being_line
by A4, AFF_4:27;
X // a * X
by A4, AFF_4:def 3;
then
X '||' a * X
by A4, A5, AFF_4:40;
then
a * X in a
by A3, A4, A5, Th9;
hence
contradiction
by A4, AFF_4:def 3; verum