let n, m be Nat; :: thesis: for Y being ref-finite ConstructorDB

for B being FinSequence of the Constrs of Y st n <= m holds

ATMOST+ (B,n) c= ATMOST+ (B,m)

let Y be ref-finite ConstructorDB ; :: thesis: for B being FinSequence of the Constrs of Y st n <= m holds

ATMOST+ (B,n) c= ATMOST+ (B,m)

let B be FinSequence of the Constrs of Y; :: thesis: ( n <= m implies ATMOST+ (B,n) c= ATMOST+ (B,m) )

assume A1: n <= m ; :: thesis: ATMOST+ (B,n) c= ATMOST+ (B,m)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ATMOST+ (B,n) or z in ATMOST+ (B,m) )

assume A2: z in ATMOST+ (B,n) ; :: thesis: z in ATMOST+ (B,m)

then z in { y where y is Element of Y : card ((y ref) \ (rng B)) <= n } by Def35;

then consider y being Element of Y such that

A3: ( z = y & card ((y ref) \ (rng B)) <= n ) ;

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

then y in { x1 where x1 is Element of Y : card ((x1 ref) \ (rng B)) <= m } ;

hence z in ATMOST+ (B,m) by A2, A3, Def35; :: thesis: verum

for B being FinSequence of the Constrs of Y st n <= m holds

ATMOST+ (B,n) c= ATMOST+ (B,m)

let Y be ref-finite ConstructorDB ; :: thesis: for B being FinSequence of the Constrs of Y st n <= m holds

ATMOST+ (B,n) c= ATMOST+ (B,m)

let B be FinSequence of the Constrs of Y; :: thesis: ( n <= m implies ATMOST+ (B,n) c= ATMOST+ (B,m) )

assume A1: n <= m ; :: thesis: ATMOST+ (B,n) c= ATMOST+ (B,m)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ATMOST+ (B,n) or z in ATMOST+ (B,m) )

assume A2: z in ATMOST+ (B,n) ; :: thesis: z in ATMOST+ (B,m)

then z in { y where y is Element of Y : card ((y ref) \ (rng B)) <= n } by Def35;

then consider y being Element of Y such that

A3: ( z = y & card ((y ref) \ (rng B)) <= n ) ;

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

then y in { x1 where x1 is Element of Y : card ((x1 ref) \ (rng B)) <= m } ;

hence z in ATMOST+ (B,m) by A2, A3, Def35; :: thesis: verum