let p be FinSequence; :: thesis: for A being set holds len (p - A) <= len p
let A be set ; :: thesis: len (p - A) <= len p
len (p - A) = (len p) - (card (p " A)) by Th66;
hence len (p - A) <= len p by XREAL_1:45; :: thesis: verum