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

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