let p be FinSequence; :: thesis: for A being set st rng (p - A) = rng p holds
A misses rng p
let A be set ; :: thesis: ( rng (p - A) = rng p implies A misses rng p )
assume rng (p - A) = rng p ; :: thesis: A misses rng p
then (rng p) \ A = rng p by Th63;
hence A misses rng p by XBOOLE_1:83; :: thesis: verum