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

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

hence z in ATLEAST A by A6, Def31; :: thesis: verum

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 meet { (x occur) where x is Element of X : x in rng A } or z in ATLEAST A )
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 ) ;

end;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

hence
z in meet { (x occur) where x is Element of X : x in rng A }
by A2, SETFAM_1:def 1; :: thesis: verumz 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;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

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

then
z in { x where x is Element of X : rng A c= x ref }
;
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;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

hence z in ATLEAST A by A6, Def31; :: thesis: verum