let V be set ; :: thesis: 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 ; :: thesis: 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)); :: thesis: 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); :: thesis: ( ( 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 ; :: thesis: (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 :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( e in v & e c= c \/ a )
thus e in v by A10; :: thesis: e c= c \/ a
thus e c= c \/ a by A8, A11; :: thesis: verum

end;

now :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( e in (StrongImpl (V,C)) . (u,v) & e c= c )
thus e in (StrongImpl (V,C)) . (u,v) by A16, Def5; :: thesis: e c= c
thus e c= c by A14, A15; :: thesis: verum

end;

hence (Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v) by Lm8; :: thesis: verum