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 Th15;
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