theorem :: LTLAXIO3:34

for P being consistent PNPair ex P1 being consistent PNPair st
( rng (P `1) c= rng (P1 `1) & rng (P `2) c= rng (P1 `2) & tau (rng P) = rng P1 )