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,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 and
A5: M is being_line and
A6: K '||' M ;
take Y = K; :: thesis: ( x = Y & Y is being_line & X '||' Y )
A7: X = M by A3, ZFMISC_1:33;
K // M by A4, A5, A6, AFF_4:40;
hence ( x = Y & Y is being_line & X '||' Y ) by A3, A4, A5, A7, AFF_4:40, ZFMISC_1:33; :: thesis: verum

end;

now

given Y being Subset of AS such that A8: x = Y and
A9: Y is being_line and
A10: X '||' Y ; :: thesis: x in LDir X
X // Y by A1, A9, A10, AFF_4:40;
then Y '||' X by A1, A9, 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, A9;
hence x in LDir X by A8, EQREL_1:27; :: 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