let E be non empty set ; :: thesis: for A, B being Ordinal st A c= B holds
Collapse (E,A) c= Collapse (E,B)
let A, B be Ordinal; :: thesis: ( A c= B implies Collapse (E,A) c= Collapse (E,B) )
assume A1: A c= B ; :: thesis: Collapse (E,A) c= Collapse (E,B)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Collapse (E,A) or x in Collapse (E,B) )
assume x in Collapse (E,A) ; :: thesis: x in Collapse (E,B)
then x in { 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 A & d1 in Collapse (E,B) ) } by Th1;
then consider d being Element of E such that
A2: d = x and
A3: for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in A & d1 in Collapse (E,B) ) ;
for d1 being Element of E st d1 in d holds
ex C being Ordinal st
( C in B & d1 in Collapse (E,C) )

proof

let d1 be Element of E; :: thesis: ( d1 in d implies ex C being Ordinal st
( C in B & d1 in Collapse (E,C) ) )
assume d1 in d ; :: thesis: ex C being Ordinal st
( C in B & d1 in Collapse (E,C) )
then consider C being Ordinal such that
A4: ( C in A & d1 in Collapse (E,C) ) by A3;
take C ; :: thesis: ( C in B & d1 in Collapse (E,C) )
thus ( C in B & d1 in Collapse (E,C) ) by A1, A4; :: thesis: verum

end;

then x in { 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 A2;
hence x in Collapse (E,B) by Th1; :: thesis: verum