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