let Y be ref-finite ConstructorDB ; :: thesis: 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; :: thesis: 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; :: thesis: ( n1 <= m1 & n2 <= m2 implies EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2) )

assume A1: ( n1 <= m1 & n2 <= m2 ) ; :: thesis: EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in EXACTLY+- (B,n1,n2) or z in EXACTLY+- (B,m1,m2) )

assume A2: z in EXACTLY+- (B,n1,n2) ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: ( n1 <= m1 & n2 <= m2 implies EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2) )

assume A1: ( n1 <= m1 & n2 <= m2 ) ; :: thesis: EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in EXACTLY+- (B,n1,n2) or z in EXACTLY+- (B,m1,m2) )

assume A2: z in EXACTLY+- (B,n1,n2) ; :: thesis: 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; :: thesis: verum