let n, m be Nat; :: thesis: for X being ConstructorDB

for A being FinSequence of the Constrs of X st n <= m holds

ATLEAST- (A,n) c= ATLEAST- (A,m)

let X be ConstructorDB ; :: thesis: for A being FinSequence of the Constrs of X st n <= m holds

ATLEAST- (A,n) c= ATLEAST- (A,m)

let A be FinSequence of the Constrs of X; :: thesis: ( n <= m implies ATLEAST- (A,n) c= ATLEAST- (A,m) )

assume A1: n <= m ; :: thesis: ATLEAST- (A,n) c= ATLEAST- (A,m)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ATLEAST- (A,n) or z in ATLEAST- (A,m) )

assume A2: z in ATLEAST- (A,n) ; :: thesis: z in ATLEAST- (A,m)

then z in { x where x is Element of X : card ((rng A) \ (x ref)) <= n } by Def34;

then consider x being Element of X such that

A3: ( z = x & card ((rng A) \ (x ref)) <= n ) ;

card ((rng A) \ (x ref)) <= m by A1, A3, XXREAL_0:2;

then x in { x1 where x1 is Element of X : card ((rng A) \ (x1 ref)) <= m } ;

hence z in ATLEAST- (A,m) by A2, A3, Def34; :: thesis: verum

for A being FinSequence of the Constrs of X st n <= m holds

ATLEAST- (A,n) c= ATLEAST- (A,m)

let X be ConstructorDB ; :: thesis: for A being FinSequence of the Constrs of X st n <= m holds

ATLEAST- (A,n) c= ATLEAST- (A,m)

let A be FinSequence of the Constrs of X; :: thesis: ( n <= m implies ATLEAST- (A,n) c= ATLEAST- (A,m) )

assume A1: n <= m ; :: thesis: ATLEAST- (A,n) c= ATLEAST- (A,m)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ATLEAST- (A,n) or z in ATLEAST- (A,m) )

assume A2: z in ATLEAST- (A,n) ; :: thesis: z in ATLEAST- (A,m)

then z in { x where x is Element of X : card ((rng A) \ (x ref)) <= n } by Def34;

then consider x being Element of X such that

A3: ( z = x & card ((rng A) \ (x ref)) <= n ) ;

card ((rng A) \ (x ref)) <= m by A1, A3, XXREAL_0:2;

then x in { x1 where x1 is Element of X : card ((rng A) \ (x1 ref)) <= m } ;

hence z in ATLEAST- (A,m) by A2, A3, Def34; :: thesis: verum