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= { () where x is Element of X : x in rng A }
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { () where x is Element of X : x in rng A } or z in {(c1 occur),(c2 occur)} )
assume z in { () 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 ;
hence z in {(c1 occur),(c2 occur)} by ; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {(c1 occur),(c2 occur)} or z in { () where x is Element of X : x in rng A } )
assume z in {(c1 occur),(c2 occur)} ; :: thesis: z in { () 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 ;
hence z in { () where x is Element of X : x in rng A } by A5; :: thesis: verum
end;
thus ATLEAST A = meet { () where x is Element of X : x in rng A } by
.= (c1 occur) AND (c2 occur) by ; :: thesis: verum