let X be ConstructorDB ; :: thesis: for A being FinSequence of the Constrs of X holds ATLEAST- (A,0) = ATLEAST A
let A be FinSequence of the Constrs of X; :: thesis: ATLEAST- (A,0) = ATLEAST A

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

suppose the carrier of X = {} ; :: thesis: ATLEAST- (A,0) = ATLEAST A

then ( ATLEAST- (A,0) = {} & ATLEAST A = {} ) ;
hence ATLEAST- (A,0) = ATLEAST A ; :: thesis: verum

end;

suppose A1: the carrier of X <> {} ; :: thesis: ATLEAST- (A,0) = ATLEAST A

then A2: ATLEAST- (A,0) = { x where x is Element of X : card ((rng A) \ (x ref)) <= 0 } by Def34;
A3: ATLEAST A = { x where x is Element of X : rng A c= x ref } by A1, Def31;
thus ATLEAST- (A,0) c= ATLEAST A :: according to XBOOLE_0:def 10 :: thesis: ATLEAST A c= ATLEAST- (A,0)

proof

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

end;

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

end;

end;