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