for E being non empty set
for A being Ordinal
for d being Element of E holds
( d /\ E c= Collapse (E,A) iff d in Collapse (E,(succ A)) )