let V be set ; :: thesis: for C being finite set
for A being Element of SubstitutionSet (V,C) holds A ^ (- A) = {}
let C be finite set ; :: thesis: for A being Element of SubstitutionSet (V,C) holds A ^ (- A) = {}
let A be Element of SubstitutionSet (V,C); :: thesis: A ^ (- A) = {}
assume A ^ (- A) <> {} ; :: thesis: 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; :: thesis: verum