theorem Th46: :: ANALMETR:46

for POS being OrtAfSp
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 )