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

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 x'' = x as Subset of (AfLines AS) ;
consider x' being set such that
A3: x' in AfLines AS and
A4: x'' = Class (LinesParallelity AS),x' by A2, EQREL_1:def 5;
consider X being Subset of AS such that
A5: x' = 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

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 5; :: 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