let AS be AffinSpace; :: thesis: for X being Subset of AS st X is being_line holds
for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )
let X be Subset of AS; :: thesis: ( X is being_line implies for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) ) )
assume A1: X is being_line ; :: thesis: for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )
let x be set ; :: thesis: ( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )

A2: now

assume x in LDir X ; :: thesis: ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y )
then x in Class (LinesParallelity AS),X by A1, Def5;
then [x,X] in LinesParallelity AS by EQREL_1:27;
then consider K, M being Subset of AS such that
A3: [x,X] = [K,M] and
A4: ( K is being_line & M is being_line & K '||' M ) ;
A5: ( x = K & X = M ) by A3, ZFMISC_1:33;
take Y = K; :: thesis: ( x = Y & Y is being_line & X '||' Y )
K // M by A4, AFF_4:40;
hence ( x = Y & Y is being_line & X '||' Y ) by A4, A5, AFF_4:40; :: thesis: verum

end;

now

given Y being Subset of AS such that A6: ( x = Y & Y is being_line & X '||' Y ) ; :: thesis: x in LDir X
X // Y by A1, A6, AFF_4:40;
then Y '||' X by A1, A6, AFF_4:40;
then [Y,X] in { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } by A1, A6;
then Y in Class (LinesParallelity AS),X by EQREL_1:27;
hence x in LDir X by A1, A6, Def5; :: thesis: verum

end;

hence ( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) ) by A2; :: thesis: verum