let V be set ; 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 ; 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)); 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); 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); ( 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 = {}
; (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 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 ;
( 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
;
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;
( e in (pseudo_compl (V,C)) . u & e c= c )thus
e in (pseudo_compl (V,C)) . u
by A2, A9, Def4;
e c= cthus
e c= c
by A7, A8;
verum end;
hence
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
by Lm8; verum