let l1 be Element of NAT ; :: thesis: for F being NAT -defined non empty finite Function st l1 in dom F holds
FirstLoc F <= l1
let F be NAT -defined non empty finite Function; :: thesis: ( l1 in dom F implies FirstLoc F <= l1 )
assume A1: l1 in dom F ; :: thesis: FirstLoc F <= l1
set M = dom F;
l1 in dom F by A1;
then min (dom F) <= l1 by XXREAL_2:def 7;
hence FirstLoc F <= l1 ; :: thesis: verum