let V be set ; :: thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds u "/\" ((StrongImpl (V,C)) . (u,v)) [= v
let C be finite set ; :: thesis: for u, v being Element of (SubstLatt (V,C)) holds u "/\" ((StrongImpl (V,C)) . (u,v)) [= v
let u, v be Element of (SubstLatt (V,C)); :: thesis: u "/\" ((StrongImpl (V,C)) . (u,v)) [= v

now :: thesis: for a being set st a in u "/\" ((StrongImpl (V,C)) . (u,v)) holds
ex b being set st
( b in v & b c= a )

reconsider u9 = u, v9 = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
let a be set ; :: thesis: ( a in u "/\" ((StrongImpl (V,C)) . (u,v)) implies ex b being set st
( b in v & b c= a ) )
assume A1: a in u "/\" ((StrongImpl (V,C)) . (u,v)) ; :: thesis: ex b being set st
( b in v & b c= a )
u "/\" ((StrongImpl (V,C)) . (u,v)) = H₁(V,C) . (u,((StrongImpl (V,C)) . (u,v))) by LATTICES:def 2
.= H₁(V,C) . (u,(mi (u9 =>> v9))) by Def5
.= mi (u9 ^ (mi (u9 =>> v9))) by SUBSTLAT:def 4
.= mi (u9 ^ (u9 =>> v9)) by SUBSTLAT:20 ;
then a in u9 ^ (u9 =>> v9) by A1, SUBSTLAT:6;
hence ex b being set st
( b in v & b c= a ) by Lm3; :: thesis: verum

end;

hence u "/\" ((StrongImpl (V,C)) . (u,v)) [= v by Lm8; :: thesis: verum