theorem :: CONMETR1:16

for X being OrtAfPl holds
( X is satisfying_PAP iff AffinStruct(# the U1 of X, the CONGR of X #) is Pappian )