let A be set ; 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); ( 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
; 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):]; ( x in u implies ex b being Element of DISJOINT_PAIRS A st
( b in v & b c= x ) )
assume A2:
x in u
; 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
; ( b in v & b c= x )
thus
( b in v & b c= x )
by A1, A3; verum