let V be set ; :: thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) st u [= v holds
for x being set st x in u holds
ex b being set st
( b in v & b c= x )
let C be finite set ; :: thesis: for u, v being Element of (SubstLatt (V,C)) st u [= v holds
for x being set st x in u holds
ex b being set st
( b in v & b c= x )
let u, v be Element of (SubstLatt (V,C)); :: thesis: ( u [= v implies for x being set st x in u holds
ex b being set st
( b in v & b c= x ) )
reconsider u9 = u, v9 = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
assume u [= v ; :: thesis: for x being set st x in u holds
ex b being set st
( b in v & b c= x )
then u = u "/\" v by LATTICES:4
.= the L_meet of (SubstLatt (V,C)) . (u,v) by LATTICES:def 2
.= mi (u9 ^ v9) by SUBSTLAT:def 4 ;
hence for x being set st x in u holds
ex b being set st
( b in v & b c= x ) by Th4; :: thesis: verum