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 object 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 object ; :: 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 Def31;
then consider a being Element of X such that
A3: ( 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
A4: ( Y = x occur & x in rng A ) ;
thus z in Y by A3, A4, Th66; :: 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 object ; :: 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 A5: z in meet { (x occur) where x is Element of X : x in rng A } ; :: thesis: z in ATLEAST A
then A6: 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 object ; :: 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 A5, SETFAM_1:def 1;
hence s in z ref by Th66; :: thesis: verum
end;
then z in { x where x is Element of X : rng A c= x ref } ;
hence z in ATLEAST A by A6, Def31; :: thesis: verum