let A be set ; :: thesis: for u, v being Element of (NormForm A) st u [= v holds

for x being Element of [:(Fin A),(Fin A):] st x in u holds

ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= x )

let u, v be Element of (NormForm A); :: thesis: ( u [= v implies for x being Element of [:(Fin A),(Fin A):] st x in u holds

ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= x ) )

assume u [= v ; :: thesis: for x being Element of [:(Fin A),(Fin A):] st x in u holds

ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= x )

then A1: v = u "\/" v by LATTICES:def 3

.= the L_join of (NormForm A) . (u,v) by LATTICES:def 1

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

let x be Element of [:(Fin A),(Fin A):]; :: thesis: ( x in u implies ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= x ) )

assume A2: x in u ; :: thesis: ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= x )

u = @ u ;

then reconsider c = x as Element of DISJOINT_PAIRS A by A2, SETWISEO:9;

c in u \/ v by A2, XBOOLE_0:def 3;

then consider b being Element of DISJOINT_PAIRS A such that

A3: ( b c= c & b in mi ((@ u) \/ (@ v)) ) by NORMFORM:41;

take b ; :: thesis: ( b in v & b c= x )

thus ( b in v & b c= x ) by A1, A3; :: thesis: verum

for x being Element of [:(Fin A),(Fin A):] st x in u holds

ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= x )

let u, v be Element of (NormForm A); :: thesis: ( u [= v implies for x being Element of [:(Fin A),(Fin A):] st x in u holds

ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= x ) )

assume u [= v ; :: thesis: for x being Element of [:(Fin A),(Fin A):] st x in u holds

ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= x )

then A1: v = u "\/" v by LATTICES:def 3

.= the L_join of (NormForm A) . (u,v) by LATTICES:def 1

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

let x be Element of [:(Fin A),(Fin A):]; :: thesis: ( x in u implies ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= x ) )

assume A2: x in u ; :: thesis: ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= x )

u = @ u ;

then reconsider c = x as Element of DISJOINT_PAIRS A by A2, SETWISEO:9;

c in u \/ v by A2, XBOOLE_0:def 3;

then consider b being Element of DISJOINT_PAIRS A such that

A3: ( b c= c & b in mi ((@ u) \/ (@ v)) ) by NORMFORM:41;

take b ; :: thesis: ( b in v & b c= x )

thus ( b in v & b c= x ) by A1, A3; :: thesis: verum