let E be non empty set ; :: thesis: for A being Ordinal
for d being Element of E holds
( d /\ E c= Collapse (E,A) iff d in Collapse (E,(succ A)) )
let A be Ordinal; :: thesis: for d being Element of E holds
( d /\ E c= Collapse (E,A) iff d in Collapse (E,(succ A)) )
let d be Element of E; :: thesis: ( d /\ E c= Collapse (E,A) iff d in Collapse (E,(succ A)) )
A1: Collapse (E,(succ A)) = { 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 succ A & d1 in Collapse (E,B) ) } by Th1;
thus ( d /\ E c= Collapse (E,A) implies d in Collapse (E,(succ A)) ) :: thesis: ( d in Collapse (E,(succ A)) implies d /\ E c= Collapse (E,A) )

proof

assume A2: for a being object st a in d /\ E holds
a in Collapse (E,A) ; :: according to TARSKI:def 3 :: thesis: d in Collapse (E,(succ A))

now :: thesis: for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in succ A & d1 in Collapse (E,B) )

let d1 be Element of E; :: thesis: ( d1 in d implies ex B being Ordinal st
( B in succ A & d1 in Collapse (E,B) ) )
assume d1 in d ; :: thesis: ex B being Ordinal st
( B in succ A & d1 in Collapse (E,B) )
then d1 in d /\ E by XBOOLE_0:def 4;
then d1 in Collapse (E,A) by A2;
hence ex B being Ordinal st
( B in succ A & d1 in Collapse (E,B) ) by ORDINAL1:6; :: thesis: verum

end;

hence d in Collapse (E,(succ A)) by A1; :: thesis: verum

end;

assume d in Collapse (E,(succ A)) ; :: thesis: d /\ E c= Collapse (E,A)
then A3: ex e1 being Element of E st
( e1 = d & ( for d1 being Element of E st d1 in e1 holds
ex B being Ordinal st
( B in succ A & d1 in Collapse (E,B) ) ) ) by A1;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in d /\ E or a in Collapse (E,A) )
assume A4: a in d /\ E ; :: thesis: a in Collapse (E,A)
then reconsider e = a as Element of E by XBOOLE_0:def 4;
a in d by A4, XBOOLE_0:def 4;
then consider B being Ordinal such that
A5: B in succ A and
A6: e in Collapse (E,B) by A3;

A7: now :: thesis: for d1 being Element of E st d1 in e holds
ex C being Ordinal st
( C in A & d1 in Collapse (E,C) )

Collapse (E,B) = { d9 where d9 is Element of E : for d1 being Element of E st d1 in d9 holds
ex C being Ordinal st
( C in B & d1 in Collapse (E,C) ) } by Th1;
then A8: ex d9 being Element of E st
( d9 = e & ( for d1 being Element of E st d1 in d9 holds
ex C being Ordinal st
( C in B & d1 in Collapse (E,C) ) ) ) by A6;
let d1 be Element of E; :: thesis: ( d1 in e implies ex C being Ordinal st
( C in A & d1 in Collapse (E,C) ) )
assume d1 in e ; :: thesis: ex C being Ordinal st
( C in A & d1 in Collapse (E,C) )
then consider C being Ordinal such that
A9: ( C in B & d1 in Collapse (E,C) ) by A8;
take C = C; :: thesis: ( C in A & d1 in Collapse (E,C) )
B c= A by A5, ORDINAL1:22;
hence ( C in A & d1 in Collapse (E,C) ) by A9; :: thesis: verum

end;

Collapse (E,A) = { 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 A & d1 in Collapse (E,B) ) } by Th1;
hence a in Collapse (E,A) by A7; :: thesis: verum