let V be non empty set ; :: thesis: for C being non empty finite set
for A being Element of SubstitutionSet (V,C) st A = {} holds
mi (- A) = Top (SubstLatt (V,C))
let C be non empty finite set ; :: thesis: for A being Element of SubstitutionSet (V,C) st A = {} holds
mi (- A) = Top (SubstLatt (V,C))
let A be Element of SubstitutionSet (V,C); :: thesis: ( A = {} implies mi (- A) = Top (SubstLatt (V,C)) )
assume A = {} ; :: thesis: mi (- A) = Top (SubstLatt (V,C))
then A1: - A = {{}} by Th10;
then - A in SubstitutionSet (V,C) by SUBSTLAT:2;
then mi (- A) = {{}} by A1, SUBSTLAT:11;
hence mi (- A) = Top (SubstLatt (V,C)) by SUBSTLAT:27; :: thesis: verum