let V be set ; :: thesis: for C being finite set
for A being Element of SubstitutionSet (V,C) holds mi (A ^ (- A)) = Bottom (SubstLatt (V,C))
let C be finite set ; :: thesis: for A being Element of SubstitutionSet (V,C) holds mi (A ^ (- A)) = Bottom (SubstLatt (V,C))
let A be Element of SubstitutionSet (V,C); :: thesis: mi (A ^ (- A)) = Bottom (SubstLatt (V,C))
mi (A ^ (- A)) = {} by Th9, SUBSTLAT:9
.= Bottom (SubstLatt (V,C)) by SUBSTLAT:26 ;
hence mi (A ^ (- A)) = Bottom (SubstLatt (V,C)) ; :: thesis: verum