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

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

.= v by A2, A6 ;

hence u [= v by LATTICES:def 3; :: thesis: verum

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

A6:
@ v c= mi ((@ u) \/ (@ v))
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;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

proof

u "\/" v =
the L_join of (NormForm A) . (u,v)
by LATTICES:def 1
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;

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

end;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

a in (@ u) \/ (@ v)
by A7, XBOOLE_0:def 3;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;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

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

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

.= v by A2, A6 ;

hence u [= v by LATTICES:def 3; :: thesis: verum