let X be ConstructorDB ; 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; 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; ( A = <*c1,c2*> implies ATLEAST A = (c1 occur) AND (c2 occur) )
assume A1:
A = <*c1,c2*>
; 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)}
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
; verum