:: deftheorem defines comp LTLAXIO4:def 6 :
for P being PNPair holds comp P = { Q where Q is consistent PNPair : Q is_completion_of P } ;