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
proof
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;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (ATLEAST A) AND (ATMOST A) or z in 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