let A be set ; :: thesis:
let u, v be Element of (NormForm A); :: thesis:
assume A1: for a being Element of DISJOINT_PAIRS A st a in u holds
ex b being Element of DISJOINT_PAIRS A st
( b in v & b c= a ) ; :: thesis:
A2: mi ((@ u) \/ (@ v)) c= @ v

let a be Element of DISJOINT_PAIRS A; :: according to HEYTING1:def 1 :: thesis:
assume A3: a in mi ((@ u) \/ (@ v)) ; :: thesis:
then a in u \/ v by NORMFORM:36;
then ( a in u or a in v ) by XBOOLE_0:def 3;
then consider b being Element of DISJOINT_PAIRS A such that
A4: b in v and
A5: b c= a by A1;
b in u \/ v by A4, XBOOLE_0:def 3;
hence a in @ v by A3, A4, A5, NORMFORM:38; :: thesis:

end;

A6: @ v c= mi ((@ u) \/ (@ v))

let a be Element of DISJOINT_PAIRS A; :: according to HEYTING1:def 1 :: thesis:
assume A7: a in @ v ; :: thesis:
then A8: a in mi (@ v) by NORMFORM:42;

A9: now :: thesis:

let b be Element of DISJOINT_PAIRS A; :: thesis:
assume that
A10: b in u \/ v and
A11: b c= a ; :: thesis:
( b in u or b in v ) by A10, XBOOLE_0:def 3;
then consider c being Element of DISJOINT_PAIRS A such that
A12: c in v and
A13: c c= b by A1;
c = a by A8, A11, A12, A13, NORMFORM:2, NORMFORM:38;
hence b = a by A11, A13, NORMFORM:1; :: thesis:

end;

a in (@ u) \/ (@ v) by A7, XBOOLE_0:def 3;
hence a in mi ((@ u) \/ (@ v)) by A9, NORMFORM:39; :: thesis:

end;

u "\/" v = the L_join of (NormForm A) . (u,v) by LATTICES:def 1
.= mi ((@ u) \/ (@ v)) by NORMFORM:def 12
.= v by A2, A6 ;
hence u [= v by LATTICES:def 3; :: thesis: