let V be set ; 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 ; 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)); u "/\" ((StrongImpl (V,C)) . (u,v)) [= v
now 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 ;
( 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))
;
ex b being set st
( b in v & b c= a )u "/\" ((StrongImpl (V,C)) . (u,v)) =
H1(
V,
C)
. (
u,
((StrongImpl (V,C)) . (u,v)))
by LATTICES:def 2
.=
H1(
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;
verum end;
hence
u "/\" ((StrongImpl (V,C)) . (u,v)) [= v
by Lm8; verum