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 )

( 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

end;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

hence
M '||' N
; :: thesis: verumfor 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;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

now :: thesis: ( M '||' N implies M // N )

hence
( M // N iff M '||' N )
by A3; :: thesis: verumconsider 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;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