theorem :: BKMODEL3:40

BK-model-Plane is satisfying_CongruenceIdentity