theorem :: ANALMETR:35

for POS being non empty ParOrtStr
for x being set holds
( x is Element of POS iff x is Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ) ;