let E be non empty set ; :: thesis: for A being Ordinal holds Collapse (E,A) c= E
let A be Ordinal; :: thesis: Collapse (E,A) c= E
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Collapse (E,A) or x in E )
assume x in Collapse (E,A) ; :: thesis: x in E
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 ex d being Element of E st
( x = d & ( for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in A & d1 in Collapse (E,B) ) ) ) ;
hence x in E ; :: thesis: verum