let V be set ; :: thesis: for C being finite set
for u being Element of holds u "/\" ((pseudo_compl V,C) . u) = Bottom (SubstLatt V,C)
let C be finite set ; :: thesis: for u being Element of holds u "/\" ((pseudo_compl V,C) . u) = Bottom (SubstLatt V,C)
let u be Element of ; :: thesis: u "/\" ((pseudo_compl V,C) . u) = Bottom (SubstLatt V,C)
reconsider u' = 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 (- u')) by Def4
.= mi (u' ^ (mi (- u'))) by SUBSTLAT:def 4
.= mi (u' ^ (- u')) by SUBSTLAT:20
.= Bottom (SubstLatt V,C) by Th17 ; :: thesis: verum