let X be ConstructorDB ; :: thesis: for A being FinSequence of the Constrs of X holds EXACTLY A = (ATLEAST A) AND (ATMOST A)

let A be FinSequence of the Constrs of X; :: thesis: EXACTLY A = (ATLEAST A) AND (ATMOST A)

thus EXACTLY A c= (ATLEAST A) AND (ATMOST A) :: according to XBOOLE_0:def 10 :: thesis: (ATLEAST A) AND (ATMOST A) c= EXACTLY A

assume A4: z in (ATLEAST A) AND (ATMOST A) ; :: thesis: z in EXACTLY A

then A5: ( z in ATLEAST A & z in ATMOST A ) by XBOOLE_0:def 4;

then z in { y where y is Element of X : y ref c= rng A } by Def32;

then consider a being Element of X such that

A6: ( z = a & a ref c= rng A ) ;

z in { y where y is Element of X : rng A c= y ref } by A5, Def31;

then consider b being Element of X such that

A7: ( z = b & rng A c= b ref ) ;

( z = a & a ref = rng A ) by A6, A7;

then z in { y where y is Element of X : y ref = rng A } ;

hence z in EXACTLY A by A4, Def33; :: thesis: verum

let A be FinSequence of the Constrs of X; :: thesis: EXACTLY A = (ATLEAST A) AND (ATMOST A)

thus EXACTLY A c= (ATLEAST A) AND (ATMOST A) :: according to XBOOLE_0:def 10 :: thesis: (ATLEAST A) AND (ATMOST A) c= EXACTLY A

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (ATLEAST A) AND (ATMOST A) or z in EXACTLY A )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in EXACTLY A or z in (ATLEAST A) AND (ATMOST A) )

assume A1: z in EXACTLY A ; :: thesis: z in (ATLEAST A) AND (ATMOST A)

then z in { x where x is Element of X : x ref = rng A } by Def33;

then consider x being Element of X such that

A2: ( z = x & x ref = rng A ) ;

z in { y where y is Element of X : rng A c= y ref } by A2;

then A3: z in ATLEAST A by A1, Def31;

z in { y where y is Element of X : y ref c= rng A } by A2;

then z in ATMOST A by A1, Def32;

hence z in (ATLEAST A) AND (ATMOST A) by A3, XBOOLE_0:def 4; :: thesis: verum

end;assume A1: z in EXACTLY A ; :: thesis: z in (ATLEAST A) AND (ATMOST A)

then z in { x where x is Element of X : x ref = rng A } by Def33;

then consider x being Element of X such that

A2: ( z = x & x ref = rng A ) ;

z in { y where y is Element of X : rng A c= y ref } by A2;

then A3: z in ATLEAST A by A1, Def31;

z in { y where y is Element of X : y ref c= rng A } by A2;

then z in ATMOST A by A1, Def32;

hence z in (ATLEAST A) AND (ATMOST A) by A3, XBOOLE_0:def 4; :: thesis: verum

assume A4: z in (ATLEAST A) AND (ATMOST A) ; :: thesis: z in EXACTLY A

then A5: ( z in ATLEAST A & z in ATMOST A ) by XBOOLE_0:def 4;

then z in { y where y is Element of X : y ref c= rng A } by Def32;

then consider a being Element of X such that

A6: ( z = a & a ref c= rng A ) ;

z in { y where y is Element of X : rng A c= y ref } by A5, Def31;

then consider b being Element of X such that

A7: ( z = b & rng A c= b ref ) ;

( z = a & a ref = rng A ) by A6, A7;

then z in { y where y is Element of X : y ref = rng A } ;

hence z in EXACTLY A by A4, Def33; :: thesis: verum