let n be Nat; :: thesis: for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds ATMOST B c= ATMOST+ (B,n)
let Y be ref-finite ConstructorDB ; :: thesis: for B being FinSequence of the Constrs of Y holds ATMOST B c= ATMOST+ (B,n)
let B be FinSequence of the Constrs of Y; :: thesis: ATMOST B c= ATMOST+ (B,n)
( ATMOST B = ATMOST+ (B,0) & 0 <= n ) by Th68, NAT_1:2;
hence ATMOST B c= ATMOST+ (B,n) by Th71; :: thesis: verum