theorem :: ANALMETR:38

for POS being OrtAfSp st AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinPlane holds
POS is OrtAfPl