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 = {{} } )
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;
assume A1: A = {} ; :: thesis: - A = {{} }
then A2: for g being Element of PFuncs V,C st g in A holds
not {} 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 A3: - A c= {{} } by PARTFUN1:122;
{} in {{} } by TARSKI:def 1;
then {} in PFuncs {} ,C by PARTFUN1:122;
then {} in PFuncs (Involved A),C by A1, Th11;
then {} in - A by A2;
then {{} } c= - A by ZFMISC_1:37;
hence - A = {{} } by A3, XBOOLE_0:def 10; :: thesis: verum