let V be set ; for C being finite set
for u being Element of (SubstLatt (V,C))
for X being set st X c= u holds
X is Element of (SubstLatt (V,C))
let C be finite set ; for u being Element of (SubstLatt (V,C))
for X being set st X c= u holds
X is Element of (SubstLatt (V,C))
let u be Element of (SubstLatt (V,C)); for X being set st X c= u holds
X is Element of (SubstLatt (V,C))
let X be set ; ( X c= u implies X is Element of (SubstLatt (V,C)) )
reconsider u9 = u as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
assume
X c= u
; X is Element of (SubstLatt (V,C))
then
X c= u9
;
then
X in SubstitutionSet (V,C)
by Lm4;
hence
X is Element of (SubstLatt (V,C))
by SUBSTLAT:def 4; verum