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,{} = { 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 {} & 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 A2: d in Collapse E,{} ; :: thesis: for d1 being Element of E holds not d1 in d
given d1 being Element of E such that A3: d1 in d ; :: thesis: contradiction
ex d' being Element of E st
( d' = d & ( for d1 being Element of E st d1 in d' holds
ex B being Ordinal st
( B in {} & d1 in Collapse E,B ) ) ) by A1, A2;
then ex B being Ordinal st
( B in {} & d1 in Collapse E,B ) by A3;
hence contradiction ; :: thesis: verum