let E be non empty set ; for d being Element of E holds
( ( for d1 being Element of E holds not d1 in d ) iff d in Collapse (E,{}) )
let d be Element of E; ( ( for d1 being Element of E holds not d1 in d ) iff d in Collapse (E,{}) )
A1:
Collapse (E,{}) = { d9 where d9 is Element of E : for d1 being Element of E st d1 in d9 holds
ex B being Ordinal st
( B in {} & d1 in Collapse (E,B) ) }
by Th1;
thus
( ( for d1 being Element of E holds not d1 in d ) implies d in Collapse (E,{}) )
( d in Collapse (E,{}) implies for d1 being Element of E holds not d1 in d )
assume
d in Collapse (E,{})
; for d1 being Element of E holds not d1 in d
then A2:
ex d9 being Element of E st
( d9 = d & ( for d1 being Element of E st d1 in d9 holds
ex B being Ordinal st
( B in {} & d1 in Collapse (E,B) ) ) )
by A1;
given d1 being Element of E such that A3:
d1 in d
; contradiction
ex B being Ordinal st
( B in {} & d1 in Collapse (E,B) )
by A3, A2;
hence
contradiction
; verum