defpred S₁[ 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 ;
then consider x being object such that
A2: x in FinSeq-Locations and
A3: not x in L ;
reconsider x = x as FinSeq-Location by A2, SCMFSA_2:def 5;
consider k being Nat such that
A4: x = fsloc k by SCMFSA_2:9;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
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