let V be set ; for C being finite set
for u, v being Element of (SubstLatt (V,C))
for a being finite Element of PFuncs (V,C) st ( for b being Element of PFuncs (V,C) st b in u holds
b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v holds
(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)
let C be finite set ; for u, v being Element of (SubstLatt (V,C))
for a being finite Element of PFuncs (V,C) st ( for b being Element of PFuncs (V,C) st b in u holds
b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v holds
(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)
let u, v be Element of (SubstLatt (V,C)); for a being finite Element of PFuncs (V,C) st ( for b being Element of PFuncs (V,C) st b in u holds
b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v holds
(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)
let a be finite Element of PFuncs (V,C); ( ( for b being Element of PFuncs (V,C) st b in u holds
b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v implies (Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v) )
assume that
A1:
for b being Element of PFuncs (V,C) st b in u holds
b tolerates a
and
A2:
u "/\" ((Atom (V,C)) . a) [= v
; (Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)
reconsider u9 = u, v9 = v, Aa = (Atom (V,C)) . a as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
A3:
now for c being set st c in u holds
ex e being set st
( e in v & e c= c \/ a )let c be
set ;
( c in u implies ex e being set st
( e in v & e c= c \/ a ) )A4:
a in Aa
by Th23;
assume A5:
c in u
;
ex e being set st
( e in v & e c= c \/ a )then A6:
c in u9
;
then reconsider c9 =
c as
Element of
PFuncs (
V,
C)
by SETWISEO:9;
c9 tolerates a
by A1, A5;
then
c \/ a in { (s1 \/ t1) where s1, t1 is Element of PFuncs (V,C) : ( s1 in u9 & t1 in Aa & s1 tolerates t1 ) }
by A5, A4;
then A7:
c \/ a in u9 ^ Aa
by SUBSTLAT:def 3;
c is
finite
by A6, Th1;
then consider b being
set such that A8:
b c= c \/ a
and A9:
b in mi (u9 ^ Aa)
by A7, SUBSTLAT:10;
b in the
L_meet of
(SubstLatt (V,C)) . (
u,
((Atom (V,C)) . a))
by A9, SUBSTLAT:def 4;
then
b in u "/\" ((Atom (V,C)) . a)
by LATTICES:def 2;
then consider d being
set such that A10:
d in v
and A11:
d c= b
by A2, Lm9;
take e =
d;
( e in v & e c= c \/ a )thus
e in v
by A10;
e c= c \/ athus
e c= c \/ a
by A8, A11;
verum end;
now for c being set st c in (Atom (V,C)) . a holds
ex e being set st
( e in (StrongImpl (V,C)) . (u,v) & e c= c )let c be
set ;
( c in (Atom (V,C)) . a implies ex e being set st
( e in (StrongImpl (V,C)) . (u,v) & e c= c ) )assume A12:
c in (Atom (V,C)) . a
;
ex e being set st
( e in (StrongImpl (V,C)) . (u,v) & e c= c )then
c = a
by Th21;
then consider b being
set such that A13:
b in u9 =>> v9
and A14:
b c= c
by A3, Th24;
c in Aa
by A12;
then
c is
finite
by Th1;
then consider d being
set such that A15:
d c= b
and A16:
d in mi (u9 =>> v9)
by A13, A14, SUBSTLAT:10;
take e =
d;
( e in (StrongImpl (V,C)) . (u,v) & e c= c )thus
e in (StrongImpl (V,C)) . (
u,
v)
by A16, Def5;
e c= cthus
e c= c
by A14, A15;
verum end;
hence
(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)
by Lm8; verum