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 )
then A2: {} in X by Th3;
thus 0-element_of V in X by A1, Th3; :: thesis: 1-element_of V in X
A3: 1 = succ 0 ;
{} \/ {{} } in X by A1, A2, Th2;
hence 1-element_of V in X by A3, ORDINAL1:def 1; :: thesis: verum