intloc 0 in Int-Locations by SCMFSA_2:def 4;
then reconsider i0 = {(intloc 0)} as finite Subset of Int-Locations by ZFMISC_1:31;
reconsider sil = (UsedIntLoc p) \/ i0 as finite Subset of Int-Locations ;
take FirstNotIn sil ; :: thesis: ex sil being finite Subset of Int-Locations st
( sil = (UsedIntLoc p) \/ {(intloc 0)} & FirstNotIn sil = FirstNotIn sil )
take sil ; :: thesis: ( sil = (UsedIntLoc p) \/ {(intloc 0)} & FirstNotIn sil = FirstNotIn sil )
thus ( sil = (UsedIntLoc p) \/ {(intloc 0)} & FirstNotIn sil = FirstNotIn sil ) ; :: thesis: verum