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 Th2;

now

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, Th26;
c = a by A4, A5, Th26;
then consider b being finite set such that
A6: b in - L and
A7: b c= c9 by A1, A3, Th19;
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, XBOOLE_1:1; :: thesis: verum

end;

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