let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for F being NAT -defined non empty lower FinPartState of holds il. (T,0) in dom F
let T be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N; :: thesis: for F being NAT -defined non empty lower FinPartState of holds il. (T,0) in dom F
let F be NAT -defined non empty lower FinPartState of ; :: thesis: il. (T,0) in dom F
consider l being set such that
A1: l in dom F by XBOOLE_0:def 1;
dom F c= NAT by RELAT_1:def 18;
then reconsider l = l as Element of NAT by A1;
consider f being Function of NAT,NAT such that
A3: f is bijective and
A4: for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,T ) and
A5: il. (T,0) = f . 0 by Def12;
rng f = NAT by A3, FUNCT_2:def 3;
then consider x being set such that
A6: x in dom f and
A7: l = f . x by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A6;
0 <= x by NAT_1:2;
then f . 0 <= f . x,T by A4;
hence il. (T,0) in dom F by A1, A5, A7, Def20; :: thesis: verum