let E be non empty set ; :: thesis: 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; :: thesis: ( ( 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,{}) ) :: thesis: ( d in Collapse (E,{}) implies for d1 being Element of E holds not d1 in d )

proof

assume for d1 being Element of E holds not d1 in d ; :: thesis: d in Collapse (E,{})
then for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in {} & d1 in Collapse (E,B) ) ;
hence d in Collapse (E,{}) by A1; :: thesis: verum

end;

assume d in Collapse (E,{}) ; :: thesis: 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 ; :: thesis: contradiction
ex B being Ordinal st
( B in {} & d1 in Collapse (E,B) ) by A3, A2;
hence contradiction ; :: thesis: verum