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