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 A1: A = <*c1,c2*> ; :: thesis: ATLEAST A = (c1 occur) AND (c2 occur)
then A2: rng A = {c1,c2} by FINSEQ_2:127;
A3: { (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 object ; :: 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
A4: ( z = x occur & x in rng A ) ;
( x = c1 or x = c2 ) by A2, A4, TARSKI:def 2;
hence z in {(c1 occur),(c2 occur)} by A4, TARSKI:def 2; :: thesis: verum

end;

let z be object ; :: 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 A5: ( z = c1 occur or z = c2 occur ) by TARSKI:def 2;
( c1 in rng A & c2 in rng A ) by A2, TARSKI:def 2;
hence z in { (x occur) where x is Element of X : x in rng A } by A5; :: thesis: verum

end;

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