let V be Universe; :: thesis: for X being Subclass of V st X is closed_wrt_A1-A7 holds
( 0-element_of V in X & 1-element_of V in X )
let X be Subclass of V; :: thesis: ( X is closed_wrt_A1-A7 implies ( 0-element_of V in X & 1-element_of V in X ) )
assume A1: X is closed_wrt_A1-A7 ; :: thesis: ( 0-element_of V in X & 1-element_of V in X )
hence 0-element_of V in X by Th3; :: thesis: 1-element_of V in X
{} in X by A1, Th3;
then ( 1 = succ 0 & {} \/ {{}} in X ) by A1, Th2;
hence 1-element_of V in X ; :: thesis: verum