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

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