let A be set ; :: thesis: for u, v being Element of (NormForm A) holds u "/\" ((StrongImpl A) . (u,v)) [= v

let u, v be Element of (NormForm A); :: thesis: u "/\" ((StrongImpl A) . (u,v)) [= v

let u, v be Element of (NormForm A); :: thesis: u "/\" ((StrongImpl A) . (u,v)) [= v

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in u "/\" ((StrongImpl A) . (u,v)) holds

ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= a )

hence
u "/\" ((StrongImpl A) . (u,v)) [= v
by Lm3; :: thesis: verumex b being Element of DISJOINT_PAIRS A st

( b in v & b c= a )

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in u "/\" ((StrongImpl A) . (u,v)) implies ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= a ) )

assume A1: a in u "/\" ((StrongImpl A) . (u,v)) ; :: thesis: ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= a )

A2: @ ((StrongImpl A) . (u,v)) = mi ((@ u) =>> (@ v)) by Def9;

u "/\" ((StrongImpl A) . (u,v)) = H_{2}(A) . (u,((StrongImpl A) . (u,v)))
by LATTICES:def 2

.= mi ((@ u) ^ (mi ((@ u) =>> (@ v)))) by A2, NORMFORM:def 12

.= mi ((@ u) ^ ((@ u) =>> (@ v))) by NORMFORM:51 ;

then a in (@ u) ^ ((@ u) =>> (@ v)) by A1, NORMFORM:36;

hence ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= a ) by Lm6; :: thesis: verum

end;( b in v & b c= a ) )

assume A1: a in u "/\" ((StrongImpl A) . (u,v)) ; :: thesis: ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= a )

A2: @ ((StrongImpl A) . (u,v)) = mi ((@ u) =>> (@ v)) by Def9;

u "/\" ((StrongImpl A) . (u,v)) = H

.= mi ((@ u) ^ (mi ((@ u) =>> (@ v)))) by A2, NORMFORM:def 12

.= mi ((@ u) ^ ((@ u) =>> (@ v))) by NORMFORM:51 ;

then a in (@ u) ^ ((@ u) =>> (@ v)) by A1, NORMFORM:36;

hence ex b being Element of DISJOINT_PAIRS A st

( b in v & b c= a ) by Lm6; :: thesis: verum