let Y be ref-finite ConstructorDB ; :: thesis: for B being FinSequence of the Constrs of Y holds ATMOST+ (B,0) = ATMOST B
let B be FinSequence of the Constrs of Y; :: thesis: ATMOST+ (B,0) = ATMOST B

per cases ( the carrier of Y = {} or the carrier of Y <> {} ) ;

suppose the carrier of Y = {} ; :: thesis: ATMOST+ (B,0) = ATMOST B

then ( ATMOST+ (B,0) = {} & ATMOST B = {} ) ;
hence ATMOST+ (B,0) = ATMOST B ; :: thesis: verum

end;

suppose A1: the carrier of Y <> {} ; :: thesis: ATMOST+ (B,0) = ATMOST B

then A2: ATMOST+ (B,0) = { y where y is Element of Y : card ((y ref) \ (rng B)) <= 0 } by Def35;
A3: ATMOST B = { y where y is Element of Y : y ref c= rng B } by A1, Def32;
thus ATMOST+ (B,0) c= ATMOST B :: according to XBOOLE_0:def 10 :: thesis: ATMOST B c= ATMOST+ (B,0)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ATMOST+ (B,0) or z in ATMOST B )
assume z in ATMOST+ (B,0) ; :: thesis: z in ATMOST B
then consider y being Element of Y such that
A4: ( z = y & card ((y ref) \ (rng B)) <= 0 ) by A2;
(y ref) \ (rng B) = {} by A4, NAT_1:3;
then y ref c= rng B by XBOOLE_1:37;
hence z in ATMOST B by A4, A3; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ATMOST B or z in ATMOST+ (B,0) )
assume z in ATMOST B ; :: thesis: z in ATMOST+ (B,0)
then consider y being Element of Y such that
A5: ( z = y & y ref c= rng B ) by A3;
(y ref) \ (rng B) = {} by A5, XBOOLE_1:37;
then card ((y ref) \ (rng B)) = 0 ;
hence z in ATMOST+ (B,0) by A2, A5; :: thesis: verum

end;

end;