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 Th14, SUBSTLAT:9
.= Bottom (SubstLatt V,C) by SUBSTLAT:26 ;
hence mi (A ^ (- A)) = Bottom (SubstLatt V,C) ; :: thesis: verum