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