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_{1}(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

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

.= mi ((@ v) \/ ((@ u) \ (@ v))) by A2, NORMFORM:def 12

.= mi (@ u) by A1, XBOOLE_1:45

.= u by NORMFORM:42 ; :: thesis: verum