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
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 )
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)) = H2(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;
hence u "/\" ((StrongImpl A) . (u,v)) [= v by Lm3; :: thesis: verum