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

now

reconsider u' = u, v' = 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 (u' =>> v')) by Def5
.= mi (u' ^ (mi (u' =>> v'))) by SUBSTLAT:def 4
.= mi (u' ^ (u' =>> v')) by SUBSTLAT:20 ;
then a in u' ^ (u' =>> v') 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