let A be set ; :: thesis:
let a be Element of DISJOINT_PAIRS A; :: thesis:
let u, w be Element of (NormForm A); :: thesis:
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:

A3: now :: thesis:

let c be Element of DISJOINT_PAIRS A; :: thesis:
assume A4: c in u ; :: thesis:
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 A1, A4, NORMFORM:35;
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 A5, NORMFORM:41;
b in H₂(A) . (u,((Atom A) . a)) by A7, NORMFORM:def 12;
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 A2, Lm2;
take e = d; :: thesis:
thus e in w by A8; :: thesis:
thus e c= c \/ a by A6, A9, NORMFORM:2; :: thesis:

end;

now :: thesis:

let c be Element of DISJOINT_PAIRS A; :: thesis:
assume c in (Atom A) . a ; :: thesis:
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 A3, Th20;
consider d being Element of DISJOINT_PAIRS A such that
A12: d c= b and
A13: d in mi ((@ u) =>> (@ w)) by A10, NORMFORM:41;
take e = d; :: thesis:
thus e in (StrongImpl A) . (u,w) by A13, Def9; :: thesis:
thus e c= c by A11, A12, NORMFORM:2; :: thesis:

end;

hence (Atom A) . a [= (StrongImpl A) . (u,w) by Lm3; :: thesis: