let Y be ref-finite ConstructorDB ; for B being FinSequence of the Constrs of Y
for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds
EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2)
let B be FinSequence of the Constrs of Y; for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds
EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2)
let n1, n2, m1, m2 be Nat; ( n1 <= m1 & n2 <= m2 implies EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2) )
assume A1:
( n1 <= m1 & n2 <= m2 )
; EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2)
let z be object ; TARSKI:def 3 ( not z in EXACTLY+- (B,n1,n2) or z in EXACTLY+- (B,m1,m2) )
assume A2:
z in EXACTLY+- (B,n1,n2)
; z in EXACTLY+- (B,m1,m2)
then
z in { y where y is Element of Y : ( card ((y ref) \ (rng B)) <= n1 & card ((rng B) \ (y ref)) <= n2 ) }
by Def36;
then consider y being Element of Y such that
A3:
( z = y & card ((y ref) \ (rng B)) <= n1 & card ((rng B) \ (y ref)) <= n2 )
;
( card ((y ref) \ (rng B)) <= m1 & card ((rng B) \ (y ref)) <= m2 )
by A1, A3, XXREAL_0:2;
then
y in { x1 where x1 is Element of Y : ( card ((x1 ref) \ (rng B)) <= m1 & card ((rng B) \ (x1 ref)) <= m2 ) }
;
hence
z in EXACTLY+- (B,m1,m2)
by A2, A3, Def36; verum