let AS be AffinSpace; :: thesis: for x being set holds
( x in Dir_of_Lines AS iff ex X being Subset of AS st
( x = LDir X & X is being_line ) )
let x be set ; :: thesis: ( x in Dir_of_Lines AS iff ex X being Subset of AS st
( x = LDir X & X is being_line ) )

A1: now :: thesis: ( x in Dir_of_Lines AS implies ex X being Subset of AS st
( x = LDir X & X is being_line ) )

assume A2: x in Dir_of_Lines AS ; :: thesis: ex X being Subset of AS st
( x = LDir X & X is being_line )
then reconsider x99 = x as Subset of (AfLines AS) ;
consider x9 being object such that
A3: x9 in AfLines AS and
A4: x99 = Class ((LinesParallelity AS),x9) by A2, EQREL_1:def 3;
consider X being Subset of AS such that
A5: x9 = X and
A6: X is being_line by A3;
take X = X; :: thesis: ( x = LDir X & X is being_line )
thus x = LDir X by A4, A5; :: thesis: X is being_line
thus X is being_line by A6; :: thesis: verum

end;

now :: thesis: ( ex X being Subset of AS st
( x = LDir X & X is being_line ) implies x in Dir_of_Lines AS )

given X being Subset of AS such that A7: x = LDir X and
A8: X is being_line ; :: thesis: x in Dir_of_Lines AS
X in AfLines AS by A8;
hence x in Dir_of_Lines AS by A7, EQREL_1:def 3; :: thesis: verum

end;

hence ( x in Dir_of_Lines AS iff ex X being Subset of AS st
( x = LDir X & X is being_line ) ) by A1; :: thesis: verum