theorem Th4: :: QC_LANG3:4

for A being QC-alphabet
for p being QC-formula of A st p is atomic holds
still_not-bound_in p = still_not-bound_in (the_arguments_of p)