theorem Th1: :: ORDINAL7:1

for X being set holds X /\ (succ X) = X