:: deftheorem defines InvPairFunc MEASURE8:def 9 :
InvPairFunc = PairFunc " ;