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

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