let A be set ; :: thesis: for u, v being Element of (NormForm A) st v in SUB u holds
v "\/" ((diff u) . v) = u
let u, v be Element of (NormForm A); :: thesis: ( v in SUB u implies v "\/" ((diff u) . v) = u )
assume A1: v in SUB u ; :: thesis: v "\/" ((diff u) . v) = u
A2: (@ u) \ (@ v) = @ ((diff u) . v) by Def11;
thus v "\/" ((diff u) . v) = H₁(A) . (v,((diff u) . v)) by LATTICES:def 1
.= mi ((@ v) \/ ((@ u) \ (@ v))) by A2, NORMFORM:def 12
.= mi (@ u) by A1, XBOOLE_1:45
.= u by NORMFORM:42 ; :: thesis: verum