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

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 Th28;
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:14;
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, Th2;
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, XBOOLE_1:1; :: thesis: verum

end;

now

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 Th26;
then consider b being set such that
A13: b in u9 =>> v9 and
A14: b c= c by A3, Th29;
c in Aa by A12;
then c is finite by Th2;
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, XBOOLE_1:1; :: thesis: verum

end;

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