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)

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 )

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_{2}(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;( 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

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

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 )

hence
(Atom A) . a [= (StrongImpl A) . (u,w)
by Lm3; :: thesis: verumex 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;( 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