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