let V be set ; :: thesis: 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 ; :: thesis: 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); :: thesis: for X being set st X c= u holds
X is Element of (SubstLatt V,C)
let X be set ; :: thesis: ( X c= u implies X is Element of (SubstLatt V,C) )
reconsider u' = u as Element of SubstitutionSet V,C by SUBSTLAT:def 4;
assume X c= u ; :: thesis: X is Element of (SubstLatt V,C)
then X c= u' ;
then X in SubstitutionSet V,C by Lm4;
hence X is Element of (SubstLatt V,C) by SUBSTLAT:def 4; :: thesis: verum