let A be set ; :: thesis: for u, v being Element of (NormForm A) st ( 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 ) ) holds
u [= v
let u, v be Element of (NormForm A); :: thesis: ( ( 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 ) ) implies u [= v )
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: u [= v
A2: mi ((@ u) \/ (@ v)) c= @ v

proof

let a be Element of DISJOINT_PAIRS A; :: according to HEYTING1:def 1 :: thesis: ( a in mi ((@ u) \/ (@ v)) implies a in @ v )
assume A3: a in mi ((@ u) \/ (@ v)) ; :: thesis: a in @ v
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: verum

end;

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

proof

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

A9: now :: thesis: for b being Element of DISJOINT_PAIRS A st b in u \/ v & b c= a holds
b = a

let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in u \/ v & b c= a implies b = a )
assume that
A10: b in u \/ v and
A11: b c= a ; :: thesis: b = a
( 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: verum

end;

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

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: verum