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