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 that
A1: M is being_line and
A2: N is being_line ; :: thesis: ( M // N iff M '||' N )
A3: now :: thesis: ( M // N implies M '||' N )
assume A4: M // N ; :: thesis: M '||' N
now :: thesis: for a being Element of AS
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 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
A5: a in N and
A6: ( A is being_line & A c= M ) ; :: thesis: a * A c= N
N = a * M by A1, A4, A5, Def3;
hence a * A c= N by A1, A6, Th33; :: thesis: verum
end;
hence M '||' N ; :: thesis: verum
end;
now :: thesis: ( M '||' N implies M // N )
consider a, b being Element of AS such that
A7: a in N and
b in N and
a <> b by A2, AFF_1:19;
A8: a * M is being_line by A1, Th27;
assume M '||' N ; :: thesis: M // N
then a * M c= N by A1, A7;
then a * M = N by A2, A8, Th33;
hence M // N by A1, Def3; :: thesis: verum
end;
hence ( M // N iff M '||' N ) by A3; :: thesis: verum