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