let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A
for u, w being Element of (NormForm A) 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 [= (StrongImpl A) . (u,w)
let a be Element of DISJOINT_PAIRS A; :: thesis: for u, w being Element of (NormForm A) 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 [= (StrongImpl A) . (u,w)
let u, w be Element of (NormForm A); :: 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 [= (StrongImpl 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 [= (StrongImpl 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 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: ( e in w & e c= c \/ a )
thus e in w by A8; :: thesis: e c= c \/ a
thus e c= c \/ a by A6, A9, NORMFORM:2; :: 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 (StrongImpl A) . (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 (StrongImpl A) . (u,w) & e c= c ) )
assume c in (Atom A) . a ; :: thesis: ex e being Element of DISJOINT_PAIRS A st
( e in (StrongImpl A) . (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 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: ( e in (StrongImpl A) . (u,w) & e c= c )
thus e in (StrongImpl A) . (u,w) by A13, Def9; :: thesis: e c= c
thus e c= c by A11, A12, NORMFORM:2; :: thesis: verum

end;

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