let AS be AffinSpace; :: thesis: for X, Y being Subset of AS st X is being_line & Y is being_line holds
( LDir X = LDir Y iff X '||' Y )
let X, Y be Subset of AS; :: thesis: ( X is being_line & Y is being_line implies ( LDir X = LDir Y iff X '||' Y ) )
assume that
A1: X is being_line and
A2: Y is being_line ; :: thesis: ( LDir X = LDir Y iff X '||' Y )
( LDir X = LDir Y iff X // Y ) by A1, A2, Th11;
hence ( LDir X = LDir Y iff X '||' Y ) by A1, A2, AFF_4:40; :: thesis: verum