let n, m be Nat; :: thesis: for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n))
let Y be ref-finite ConstructorDB ; :: thesis: for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n))
let B be FinSequence of the Constrs of Y; :: thesis: EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n))
thus EXACTLY+- (B,n,m) c= (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) :: according to XBOOLE_0:def 10 :: thesis: (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) c= EXACTLY+- (B,n,m)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in EXACTLY+- (B,n,m) or z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) )
assume A1: z in EXACTLY+- (B,n,m) ; :: thesis: z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n))
then z in { x where x is Element of Y : ( card ((x ref) \ (rng B)) <= n & card ((rng B) \ (x ref)) <= m ) } by DefExactlyPlusMinus;
then consider x being Element of Y such that
A2: ( z = x & card ((x ref) \ (rng B)) <= n & card ((rng B) \ (x ref)) <= m ) ;
z in { y where y is Element of Y : card ((rng B) \ (y ref)) <= m } by A2;
then A3: z in ATLEAST- (B,m) by A1, DefAtleastMinus;
z in { y where y is Element of Y : card ((y ref) \ (rng B)) <= n } by A2;
then z in ATMOST+ (B,n) by A1, DefAtmostPlus;
hence z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) or z in EXACTLY+- (B,n,m) )
assume A6: z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) ; :: thesis: z in EXACTLY+- (B,n,m)
then A4: ( z in ATLEAST- (B,m) & z in ATMOST+ (B,n) ) by XBOOLE_0:def 4;
then z in { y where y is Element of Y : card ((y ref) \ (rng B)) <= n } by DefAtmostPlus;
then A5: ex y being Element of Y st
( z = y & card ((y ref) \ (rng B)) <= n ) ;
z in { y where y is Element of Y : card ((rng B) \ (y ref)) <= m } by A4, DefAtleastMinus;
then ex y being Element of Y st
( z = y & card ((rng B) \ (y ref)) <= m ) ;
then z in { y where y is Element of Y : ( card ((y ref) \ (rng B)) <= n & card ((rng B) \ (y ref)) <= m ) } by A5;
hence z in EXACTLY+- (B,n,m) by A6, DefExactlyPlusMinus; :: thesis: verum