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:51;
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 14
.= mi ((@ u) ^ (- (@ u))) by NORMFORM:75
.= mi zero by Th26
.= {} by NORMFORM:64, XBOOLE_1:3
.= Bottom (NormForm A) by NORMFORM:86 ; :: thesis: verum