let POS be OrtAfSp; :: thesis: for M, N being Subset of POS
for M9, N9 being Subset of AffinStruct(# the carrier of POS, the CONGR of POS #) st M = M9 & N = N9 holds
( M // N iff M9 // N9 )
let M, N be Subset of POS; :: thesis: for M9, N9 being Subset of AffinStruct(# the carrier of POS, the CONGR of POS #) st M = M9 & N = N9 holds
( M // N iff M9 // N9 )
let M9, N9 be Subset of AffinStruct(# the carrier of POS, the CONGR of POS #); :: thesis: ( M = M9 & N = N9 implies ( M // N iff M9 // N9 ) )
assume A1: ( M = M9 & N = N9 ) ; :: thesis: ( M // N iff M9 // N9 )

hereby :: thesis: ( M9 // N9 implies M // N )

assume M // N ; :: thesis: M9 // N9
then consider a, b, c, d being Element of POS such that
A2: ( a <> b & c <> d ) and
A3: ( M = Line (a,b) & N = Line (c,d) ) and
A4: a,b // c,d ;
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
A5: a9,b9 // c9,d9 by A4, Th36;
( M9 = Line (a9,b9) & N9 = Line (c9,d9) ) by A1, A3, Th41;
hence M9 // N9 by A2, A5, AFF_1:37; :: thesis: verum

end;

assume M9 // N9 ; :: thesis: M // N
then consider a9, b9, c9, d9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A6: ( a9 <> b9 & c9 <> d9 ) and
A7: a9,b9 // c9,d9 and
A8: ( M9 = Line (a9,b9) & N9 = Line (c9,d9) ) by AFF_1:37;
reconsider a = a9, b = b9, c = c9, d = d9 as Element of POS ;
A9: a,b // c,d by A7, Th36;
( M = Line (a,b) & N = Line (c,d) ) by A1, A8, Th41;
hence M // N by A6, A9; :: thesis: verum