theorem :: ANALMETR:42

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