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 set ; :: 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