let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for F being empty FinPartState of S holds F is lower
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: for F being empty FinPartState of S holds F is lower
let F be empty FinPartState of S; :: thesis: F is lower
let l be Element of NAT ; :: according to AMI_WSTD:def 20 :: thesis: ( l in dom F implies for m being Element of NAT st m <= l,S holds
m in dom F )
assume l in dom F ; :: thesis: for m being Element of NAT st m <= l,S holds
m in dom F
hence for m being Element of NAT st m <= l,S holds
m in dom F ; :: thesis: verum