defpred S₁[ Element of NAT ] means not fsloc $1 in L;
set sn = { k where k is Element of NAT : S₁[k] } ;
A1: { k where k is Element of NAT : S₁[k] } is Subset of NAT from DOMAIN_1:sch 7();
not FinSeq-Locations c= L by SCMFSA_2:23;
then consider x being set such that
A2: x in FinSeq-Locations and
A3: not x in L by TARSKI:def 3;
reconsider x = x as FinSeq-Location by A2, SCMFSA_2:12;
consider k being Element of NAT such that
A4: x = fsloc k by SCMFSA_2:20;
k in { k where k is Element of NAT : S₁[k] } by A3, A4;
then reconsider sn = { k where k is Element of NAT : S₁[k] } as non empty Subset of NAT by A1;
take fsloc (min sn) ; :: thesis: ex sn being non empty Subset of NAT st
( fsloc (min sn) = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } )
take sn ; :: thesis: ( fsloc (min sn) = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } )
thus ( fsloc (min sn) = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } ) ; :: thesis: verum