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