let H be ZF-formula; :: thesis: for E being non empty set st H is universal holds
for f being Function of VAR ,E holds
( ( f in St (the_scope_of H),E & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H = y ) holds
g in St (the_scope_of H),E ) ) iff f in St H,E )
let E be non empty set ; :: thesis: ( H is universal implies for f being Function of VAR ,E holds
( ( f in St (the_scope_of H),E & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H = y ) holds
g in St (the_scope_of H),E ) ) iff f in St H,E ) )
assume H is universal ; :: thesis: for f being Function of VAR ,E holds
( ( f in St (the_scope_of H),E & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H = y ) holds
g in St (the_scope_of H),E ) ) iff f in St H,E )
then H = All (bound_in H),(the_scope_of H) by ZF_LANG:62;
hence for f being Function of VAR ,E holds
( ( f in St (the_scope_of H),E & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H = y ) holds
g in St (the_scope_of H),E ) ) iff f in St H,E ) by Th6; :: thesis: verum