let A be set ; :: thesis: for u, v being Element of () 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 (); :: 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 () . (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 ;
c in u \/ v by ;
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