:: deftheorem defines ^ LTLAXIO3:def 9 :
for P being PNPair holds P ^ = ((con (P `1)) /. (len (con (P `1)))) '&&' ((con (nega (P `2))) /. (len (con (nega (P `2)))));