let V be set ; :: thesis: for C being finite set
for A being Element of SubstitutionSet V,C st A = {} holds
- A = {{} }
let C be finite set ; :: thesis: for A being Element of SubstitutionSet V,C st A = {} holds
- A = {{} }
let A be Element of SubstitutionSet V,C; :: thesis: ( A = {} implies - A = {{} } )
assume A1: A = {} ; :: thesis: - A = {{} }
defpred S₁[ Element of PFuncs (Involved A),C] means for g being Element of PFuncs V,C st g in A holds
not $1 tolerates g;
{ xx where xx is Element of PFuncs (Involved A),C : S₁[xx] } c= PFuncs (Involved A),C from FRAENKEL:sch 10();
then - A c= PFuncs {} ,C by A1, Th11;
then A2: - A c= {{} } by PARTFUN1:122;
{} in - A

proof

{} in {{} } by TARSKI:def 1;
then {} in PFuncs {} ,C by PARTFUN1:122;
then A3: {} in PFuncs (Involved A),C by A1, Th11;
for g being Element of PFuncs V,C st g in A holds
not {} tolerates g by A1;
hence {} in - A by A3; :: thesis: verum

end;

then {{} } c= - A by ZFMISC_1:37;
hence - A = {{} } by A2, XBOOLE_0:def 10; :: thesis: verum