let A be set ; :: thesis: for u being Element of (NormForm A) holds u "/\" ((pseudo_compl A) . u) = Bottom (NormForm A)
let u be Element of (NormForm A); :: thesis: u "/\" ((pseudo_compl A) . u) = Bottom (NormForm A)
reconsider zero = {} as Element of Normal_forms_on A by NORMFORM:31;
A1: @ ((pseudo_compl A) . u) = mi (- (@ u)) by Def8;
thus u "/\" ((pseudo_compl A) . u) = H₂(A) . (u,((pseudo_compl A) . u)) by LATTICES:def 2
.= mi ((@ u) ^ (mi (- (@ u)))) by A1, NORMFORM:def 12
.= mi ((@ u) ^ (- (@ u))) by NORMFORM:51
.= mi zero by Th21
.= {} by NORMFORM:40, XBOOLE_1:3
.= Bottom (NormForm A) by NORMFORM:57 ; :: thesis: verum