for p, q being XFinSequence holds p c= p ^ q