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, Th9 ;
hence u [= v by LATTICES:21; :: thesis: verum