let POS be OrtAfSp; :: thesis: for M, N being Subset of
for M', N' being Subset of st M = M' & N = N' holds
( M // N iff M' // N' )
let M, N be Subset of ; :: thesis: for M', N' being Subset of st M = M' & N = N' holds
( M // N iff M' // N' )
let M', N' be Subset of ; :: thesis: ( M = M' & N = N' implies ( M // N iff M' // N' ) )
assume A1: ( M = M' & N = N' ) ; :: thesis: ( M // N iff M' // N' )

hereby :: thesis: ( M' // N' implies M // N )

assume M // N ; :: thesis: M' // N'
then consider a, b, c, d being Element of such that
A2: ( a <> b & c <> d ) and
A3: ( M = Line a,b & N = Line c,d ) and
A4: a,b // c,d by Def16;
reconsider a' = a, b' = b, c' = c, d' = d as Element of ;
A5: a',b' // c',d' by A4, Th48;
( M' = Line a',b' & N' = Line c',d' ) by A1, A3, Th56;
hence M' // N' by A2, A5, AFF_1:51; :: thesis: verum

end;

assume M' // N' ; :: thesis: M // N
then consider a', b', c', d' being Element of such that
A6: ( a' <> b' & c' <> d' ) and
A7: a',b' // c',d' and
A8: ( M' = Line a',b' & N' = Line c',d' ) by AFF_1:51;
reconsider a = a', b = b', c = c', d = d' as Element of ;
A9: a,b // c,d by A7, Th48;
( M = Line a,b & N = Line c,d ) by A1, A8, Th56;
hence M // N by A6, A9, Def16; :: thesis: verum