theorem :: CONMETR1:13

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