let A be set ; :: thesis: for u, v being Element of () 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 (); :: 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
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 ;
hence a in @ v by ; :: thesis: verum
end;
A6: @ v c= mi ((@ u) \/ (@ v))
proof
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;
A9: now :: thesis: for b being Element of DISJOINT_PAIRS A st b in u \/ v & b c= a holds
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 ;
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 ;
hence b = a by ; :: thesis: verum
end;
a in (@ u) \/ (@ v) by ;
hence a in mi ((@ u) \/ (@ v)) by ; :: thesis: verum
end;
u "\/" v = the L_join of () . (u,v) by LATTICES:def 1
.= mi ((@ u) \/ (@ v)) by NORMFORM:def 12
.= v by A2, A6 ;
hence u [= v by LATTICES:def 3; :: thesis: verum