for n being Nat
for p being XFinSequence holds (p | n) ^ (p /^ n) = p