let V be Universe; :: thesis: for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 holds
n in X
let X be Subclass of V; :: thesis: for n being Element of omega st X is closed_wrt_A1-A7 holds
n in X
let n be Element of omega ; :: thesis: ( X is closed_wrt_A1-A7 implies n in X )
assume X is closed_wrt_A1-A7 ; :: thesis: n in X
then omega c= X by Th7;
hence n in X by TARSKI:def 3; :: thesis: verum