let n, m be Nat; 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 ; 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; 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; verum