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