:: deftheorem Def1 defines Collapse ZF_COLLA:def 1 :
for E being non empty set
for A being Ordinal
for b₃ being set holds
( b₃ = Collapse (E,A) iff ex L being Sequence st
( b₃ = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} ) } & dom L = A & ( for B being Ordinal st B in A holds
L . B = { d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} ) } ) ) );