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

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 <> {} )
;

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)

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;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 or z in ATMOST+ (B,0) )
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;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

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