theorem :: MMLQUER2:17

for x being set
for A being FinSequence st A <- x = 0 holds
x nin rng A