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)

assume A4: z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) ; :: thesis: z in EXACTLY+- (B,n,m)

then A5: ( 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 Def35;

then A6: 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 A5, Def34;

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 A6;

hence z in EXACTLY+- (B,n,m) by A4, Def36; :: thesis: verum

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 object ; :: according to TARSKI:def 3 :: thesis: ( not z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) or z in EXACTLY+- (B,n,m) )
let z be object ; :: 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 Def36;

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, Def34;

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, Def35;

hence z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) by A3, XBOOLE_0:def 4; :: thesis: verum

end;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 Def36;

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, Def34;

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, Def35;

hence z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) by A3, XBOOLE_0:def 4; :: thesis: verum

assume A4: z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) ; :: thesis: z in EXACTLY+- (B,n,m)

then A5: ( 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 Def35;

then A6: 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 A5, Def34;

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 A6;

hence z in EXACTLY+- (B,n,m) by A4, Def36; :: thesis: verum