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 )
A3: LDir Y = Class ((LinesParallelity AS),Y) ;
A4: Y in AfLines AS by A2;
A5: now :: thesis: ( LDir X = LDir Y implies X // Y )
assume LDir X = LDir Y ; :: thesis: X // Y
then X in Class ((LinesParallelity AS),Y) by A4, EQREL_1:23;
then ex Y9 being Subset of AS st
( X = Y9 & Y9 is being_line & Y '||' Y9 ) by A2, A3, Th9;
hence X // Y by A2, AFF_4:40; :: thesis: verum
end;
A6: LDir X = Class ((LinesParallelity AS),X) ;
A7: X in AfLines AS by A1;
now :: thesis: ( X // Y implies LDir X = LDir Y )
assume X // Y ; :: thesis: LDir X = LDir Y
then X '||' Y by A1, A2, AFF_4:40;
then Y in Class ((LinesParallelity AS),X) by A1, A2, A6, Th9;
hence LDir X = LDir Y by A7, EQREL_1:23; :: thesis: verum
end;
hence ( LDir X = LDir Y iff X // Y ) by A5; :: thesis: verum