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 l1, l2 being Element of NAT holds
( locnum l1,T <= locnum l2,T iff l1 <= l2,T )
let T be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N; :: thesis: for l1, l2 being Element of NAT holds
( locnum l1,T <= locnum l2,T iff l1 <= l2,T )
let l1, l2 be Element of NAT ; :: thesis: ( locnum l1,T <= locnum l2,T iff l1 <= l2,T )
( il. T,(locnum l1,T) = l1 & il. T,(locnum l2,T) = l2 ) by Def13;
hence ( locnum l1,T <= locnum l2,T iff l1 <= l2,T ) by Th28; :: thesis: verum