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)}

.= (c1 occur) AND (c2 occur) by A3, SETFAM_1:11 ; :: thesis: verum

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 ATLEAST A =
meet { (x occur) where x is Element of X : x in rng A }
by A1, Th78
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 }

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

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 } )
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;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

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

.= (c1 occur) AND (c2 occur) by A3, SETFAM_1:11 ; :: thesis: verum