let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A
for u, w being Element of () st ( for b being Element of DISJOINT_PAIRS A st b in u holds
b \/ a in DISJOINT_PAIRS A ) & u "/\" ((Atom A) . a) [= w holds
(Atom A) . a [= () . (u,w)

let a be Element of DISJOINT_PAIRS A; :: thesis: for u, w being Element of () st ( for b being Element of DISJOINT_PAIRS A st b in u holds
b \/ a in DISJOINT_PAIRS A ) & u "/\" ((Atom A) . a) [= w holds
(Atom A) . a [= () . (u,w)

let u, w be Element of (); :: thesis: ( ( for b being Element of DISJOINT_PAIRS A st b in u holds
b \/ a in DISJOINT_PAIRS A ) & u "/\" ((Atom A) . a) [= w implies (Atom A) . a [= () . (u,w) )

assume that
A1: for b being Element of DISJOINT_PAIRS A st b in u holds
b \/ a in DISJOINT_PAIRS A and
A2: u "/\" ((Atom A) . a) [= w ; :: thesis: (Atom A) . a [= () . (u,w)
A3: now :: thesis: for c being Element of DISJOINT_PAIRS A st c in u holds
ex e being Element of DISJOINT_PAIRS A st
( e in w & e c= c \/ a )
let c be Element of DISJOINT_PAIRS A; :: thesis: ( c in u implies ex e being Element of DISJOINT_PAIRS A st
( e in w & e c= c \/ a ) )

assume A4: c in u ; :: thesis: ex e being Element of DISJOINT_PAIRS A st
( e in w & e c= c \/ a )

then A5: c \/ a is Element of DISJOINT_PAIRS A by A1;
a in @ ((Atom A) . a) by Th7;
then c \/ a in (@ u) ^ (@ ((Atom A) . a)) by ;
then consider b being Element of DISJOINT_PAIRS A such that
A6: b c= c \/ a and
A7: b in mi ((@ u) ^ (@ ((Atom A) . a))) by ;
b in H2(A) . (u,((Atom A) . a)) by ;
then b in u "/\" ((Atom A) . a) by LATTICES:def 2;
then consider d being Element of DISJOINT_PAIRS A such that
A8: d in w and
A9: d c= b by ;
take e = d; :: thesis: ( e in w & e c= c \/ a )
thus e in w by A8; :: thesis: e c= c \/ a
thus e c= c \/ a by ; :: thesis: verum
end;
now :: thesis: for c being Element of DISJOINT_PAIRS A st c in (Atom A) . a holds
ex e being Element of DISJOINT_PAIRS A st
( e in () . (u,w) & e c= c )
let c be Element of DISJOINT_PAIRS A; :: thesis: ( c in (Atom A) . a implies ex e being Element of DISJOINT_PAIRS A st
( e in () . (u,w) & e c= c ) )

assume c in (Atom A) . a ; :: thesis: ex e being Element of DISJOINT_PAIRS A st
( e in () . (u,w) & e c= c )

then c = a by Th6;
then consider b being Element of DISJOINT_PAIRS A such that
A10: b in (@ u) =>> (@ w) and
A11: b c= c by ;
consider d being Element of DISJOINT_PAIRS A such that
A12: d c= b and
A13: d in mi ((@ u) =>> (@ w)) by ;
take e = d; :: thesis: ( e in () . (u,w) & e c= c )
thus e in () . (u,w) by ; :: thesis: e c= c
thus e c= c by ; :: thesis: verum
end;
hence (Atom A) . a [= () . (u,w) by Lm3; :: thesis: verum