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

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

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)

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;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 or z in ATLEAST- (A,0) )
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;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

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