let V be set ; for C being finite set
for A being Element of SubstitutionSet (V,C) holds A ^ (- A) = {}
let C be finite set ; for A being Element of SubstitutionSet (V,C) holds A ^ (- A) = {}
let A be Element of SubstitutionSet (V,C); A ^ (- A) = {}
assume
A ^ (- A) <> {}
; contradiction
then consider x being object such that
A1:
x in A ^ (- A)
by XBOOLE_0:def 1;
x in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in - A & s tolerates t ) }
by A1, SUBSTLAT:def 3;
then consider s1, t1 being Element of PFuncs (V,C) such that
x = s1 \/ t1
and
A2:
s1 in A
and
A3:
t1 in - A
and
A4:
s1 tolerates t1
;
ex f1 being Element of PFuncs ((Involved A),C) st
( f1 = t1 & ( for g being Element of PFuncs (V,C) st g in A holds
not f1 tolerates g ) )
by A3;
hence
contradiction
by A2, A4; verum