let V be set ; :: thesis: for C being finite set
for u being Element of (SubstLatt (V,C))
for K, L being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
let C be finite set ; :: thesis: for u being Element of (SubstLatt (V,C))
for K, L being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
let u be Element of (SubstLatt (V,C)); :: thesis: for K, L being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
let K, L be Element of SubstitutionSet (V,C); :: thesis: for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
let a be Element of PFuncs (V,C); :: thesis: ( K = {a} & L = u & L ^ K = {} implies (Atom (V,C)) . a [= (pseudo_compl (V,C)) . u )
assume that
A1: K = {a} and
A2: L = u and
A3: L ^ K = {} ; :: thesis: (Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
a in K by A1, TARSKI:def 1;
then A4: a is finite by Th1;

now :: thesis: for c being set st c in (Atom (V,C)) . a holds
ex e being set st
( e in (pseudo_compl (V,C)) . u & e c= c )

let c be set ; :: thesis: ( c in (Atom (V,C)) . a implies ex e being set st
( e in (pseudo_compl (V,C)) . u & e c= c ) )
assume A5: c in (Atom (V,C)) . a ; :: thesis: ex e being set st
( e in (pseudo_compl (V,C)) . u & e c= c )
then reconsider c9 = c as Element of PFuncs (V,C) by A4, Th21;
c = a by A4, A5, Th21;
then consider b being finite set such that
A6: b in - L and
A7: b c= c9 by A1, A3, Th14;
consider d being set such that
A8: d c= b and
A9: d in mi (- L) by A6, SUBSTLAT:10;
take e = d; :: thesis: ( e in (pseudo_compl (V,C)) . u & e c= c )
thus e in (pseudo_compl (V,C)) . u by A2, A9, Def4; :: thesis: e c= c
thus e c= c by A7, A8; :: thesis: verum

end;

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