let X be ConstructorDB ; :: thesis: for A being FinSequence of the Constrs of X holds EXACTLY A = () AND ()
let A be FinSequence of the Constrs of X; :: thesis: EXACTLY A = () AND ()
thus EXACTLY A c= () AND () :: according to XBOOLE_0:def 10 :: thesis: () AND () c= EXACTLY A
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in EXACTLY A or z in () AND () )
assume A1: z in EXACTLY A ; :: thesis: z in () AND ()
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 ;
z in { y where y is Element of X : y ref c= rng A } by A2;
then z in ATMOST A by ;
hence z in () AND () by ; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in () AND () or z in EXACTLY A )
assume A4: z in () AND () ; :: thesis:
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 ;
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 ; :: thesis: verum