reconsider i0 = {(intloc 0)} as finite Subset of Int-Locations ;
reconsider sil = (UsedILoc p) \/ i0 as finite Subset of Int-Locations ;
take FirstNotIn sil ; :: thesis: ex sil being finite Subset of Int-Locations st
( sil = (UsedILoc p) \/ {(intloc 0)} & FirstNotIn sil = FirstNotIn sil )
take sil ; :: thesis: ( sil = (UsedILoc p) \/ {(intloc 0)} & FirstNotIn sil = FirstNotIn sil )
thus ( sil = (UsedILoc p) \/ {(intloc 0)} & FirstNotIn sil = FirstNotIn sil ) ; :: thesis: verum