let AS be AffinSpace; :: thesis: for M, N being Subset of AS st M is being_line & N is being_line holds
( M // N iff M '||' N )
let M, N be Subset of AS; :: thesis: ( M is being_line & N is being_line implies ( M // N iff M '||' N ) )
assume A1: ( M is being_line & N is being_line ) ; :: thesis: ( M // N iff M '||' N )

A2: now

assume A3: M // N ; :: thesis: M '||' N

now

let a be Element of AS; :: thesis: for A being Subset of AS st a in N & A is being_line & A c= M holds
a * A c= N
let A be Subset of AS; :: thesis: ( a in N & A is being_line & A c= M implies a * A c= N )
assume that
A4: a in N and
A5: ( A is being_line & A c= M ) ; :: thesis: a * A c= N
N = a * M by A1, A3, A4, Def3;
hence a * A c= N by A1, A5, Th33; :: thesis: verum

end;

hence M '||' N by Def4; :: thesis: verum

end;

now

assume A6: M '||' N ; :: thesis: M // N
consider a, b being Element of AS such that
A7: a in N and
( b in N & a <> b ) by A1, AFF_1:31;
A8: a * M c= N by A1, A6, A7, Def4;
a * M is being_line by A1, Th27;
then a * M = N by A1, A8, Th33;
hence M // N by A1, Def3; :: thesis: verum

end;

hence ( M // N iff M '||' N ) by A2; :: thesis: verum