let X be ConstructorDB ; :: thesis: for A being FinSequence of the Constrs of X
for c1, c2 being Element of X st A = <*c1,c2*> holds
ATLEAST A = (c1 occur) AND (c2 occur)
let A be FinSequence of the Constrs of X; :: thesis: for c1, c2 being Element of X st A = <*c1,c2*> holds
ATLEAST A = (c1 occur) AND (c2 occur)
let c1, c2 be Element of X; :: thesis: ( A = <*c1,c2*> implies ATLEAST A = (c1 occur) AND (c2 occur) )
assume Z0: A = <*c1,c2*> ; :: thesis: ATLEAST A = (c1 occur) AND (c2 occur)
then A0: rng A = {c1,c2} by FINSEQ_2:127;
A1: { (x occur) where x is Element of X : x in rng A } = {(c1 occur),(c2 occur)}

proof

thus { (x occur) where x is Element of X : x in rng A } c= {(c1 occur),(c2 occur)} :: according to XBOOLE_0:def 10 :: thesis: {(c1 occur),(c2 occur)} c= { (x occur) where x is Element of X : x in rng A }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { (x occur) where x is Element of X : x in rng A } or z in {(c1 occur),(c2 occur)} )
assume z in { (x occur) where x is Element of X : x in rng A } ; :: thesis: z in {(c1 occur),(c2 occur)}
then consider x being Element of X such that
A2: ( z = x occur & x in rng A ) ;
( x = c1 or x = c2 ) by A0, A2, TARSKI:def 2;
hence z in {(c1 occur),(c2 occur)} by A2, TARSKI:def 2; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {(c1 occur),(c2 occur)} or z in { (x occur) where x is Element of X : x in rng A } )
assume z in {(c1 occur),(c2 occur)} ; :: thesis: z in { (x occur) where x is Element of X : x in rng A }
then A3: ( z = c1 occur or z = c2 occur ) by TARSKI:def 2;
( c1 in rng A & c2 in rng A ) by A0, TARSKI:def 2;
hence z in { (x occur) where x is Element of X : x in rng A } by A3; :: thesis: verum

end;

thus ATLEAST A = meet { (x occur) where x is Element of X : x in rng A } by Z0, Th65
.= (c1 occur) AND (c2 occur) by A1, SETFAM_1:11 ; :: thesis: verum