let V be set ; :: thesis: for C being finite set
for u being Element of (SubstLatt (V,C)) holds u "/\" ((pseudo_compl (V,C)) . u) = Bottom (SubstLatt (V,C))
let C be finite set ; :: thesis: for u being Element of (SubstLatt (V,C)) holds u "/\" ((pseudo_compl (V,C)) . u) = Bottom (SubstLatt (V,C))
let u be Element of (SubstLatt (V,C)); :: thesis: u "/\" ((pseudo_compl (V,C)) . u) = Bottom (SubstLatt (V,C))
reconsider u9 = u as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
thus u "/\" ((pseudo_compl (V,C)) . u) = H₁(V,C) . (u,((pseudo_compl (V,C)) . u)) by LATTICES:def 2
.= H₁(V,C) . (u,(mi (- u9))) by Def4
.= mi (u9 ^ (mi (- u9))) by SUBSTLAT:def 4
.= mi (u9 ^ (- u9)) by SUBSTLAT:20
.= Bottom (SubstLatt (V,C)) by Th12 ; :: thesis: verum