let n be Nat; :: thesis: for X being ConstructorDB

for A being FinSequence of the Constrs of X holds ATLEAST A c= ATLEAST- (A,n)

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

let A be FinSequence of the Constrs of X; :: thesis: ATLEAST A c= ATLEAST- (A,n)

( ATLEAST A = ATLEAST- (A,0) & 0 <= n ) by Th67, NAT_1:2;

hence ATLEAST A c= ATLEAST- (A,n) by Th70; :: thesis: verum

for A being FinSequence of the Constrs of X holds ATLEAST A c= ATLEAST- (A,n)

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

let A be FinSequence of the Constrs of X; :: thesis: ATLEAST A c= ATLEAST- (A,n)

( ATLEAST A = ATLEAST- (A,0) & 0 <= n ) by Th67, NAT_1:2;

hence ATLEAST A c= ATLEAST- (A,n) by Th70; :: thesis: verum