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 & ( 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
A3: ( C in A & d1 in Collapse E,C ) by A2;
take C ; :: thesis: ( C in B & d1 in Collapse E,C )
thus ( C in B & d1 in Collapse E,C ) by A1, A3; :: thesis: verum

end;

then x in { d' where d' is Element of E : for d1 being Element of E st d1 in d' 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