let X be ConstructorDB ; :: thesis: for A being FinSequence of the Constrs of X st A <> {} holds
ATLEAST A = meet { (x occur) where x is Element of X : x in rng A }
let A be FinSequence of the Constrs of X; :: thesis: ( A <> {} implies ATLEAST A = meet { (x occur) where x is Element of X : x in rng A } )
assume A <> {} ; :: thesis: ATLEAST A = meet { (x occur) where x is Element of X : x in rng A }
then rng A <> {} by RELAT_1:41;
then consider s being set such that
A1: s in rng A by XBOOLE_0:def 1;
( s in the Constrs of X & the Constrs of X c= the carrier of X ) by A1;
then reconsider s = s as Element of X ;
A2: s occur in { (x occur) where x is Element of X : x in rng A } by A1;
thus ATLEAST A c= meet { (x occur) where x is Element of X : x in rng A } :: according to XBOOLE_0:def 10 :: thesis: meet { (x occur) where x is Element of X : x in rng A } c= ATLEAST A

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in ATLEAST A or z in meet { (x occur) where x is Element of X : x in rng A } )
assume z in ATLEAST A ; :: thesis: z in meet { (x occur) where x is Element of X : x in rng A }
then z in { y where y is Element of X : rng A c= y ref } by DefAtleast;
then consider a being Element of X such that
A5: ( z = a & rng A c= a ref ) ;

now :: thesis: for Y being set st Y in { (x occur) where x is Element of X : x in rng A } holds
z in Y

let Y be set ; :: thesis: ( Y in { (x occur) where x is Element of X : x in rng A } implies z in Y )
assume Y in { (x occur) where x is Element of X : x in rng A } ; :: thesis: z in Y
then consider x being Element of X such that
A3: ( Y = x occur & x in rng A ) ;
thus z in Y by A5, A3, Th10; :: thesis: verum

end;

hence z in meet { (x occur) where x is Element of X : x in rng A } by A2, SETFAM_1:def 1; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in meet { (x occur) where x is Element of X : x in rng A } or z in ATLEAST A )
assume A6: z in meet { (x occur) where x is Element of X : x in rng A } ; :: thesis: z in ATLEAST A
then A8: z in s occur by A2, SETFAM_1:def 1;
then reconsider z = z as Element of X ;
rng A c= z ref

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in rng A or s in z ref )
assume A7: s in rng A ; :: thesis: s in z ref
then s in the Constrs of X ;
then reconsider s = s as Element of X ;
s occur in { (x occur) where x is Element of X : x in rng A } by A7;
then z in s occur by A6, SETFAM_1:def 1;
hence s in z ref by Th10; :: thesis: verum

end;

then z in { x where x is Element of X : rng A c= x ref } ;
hence z in ATLEAST A by A8, DefAtleast; :: thesis: verum