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