theorem :: WAYBEL21:11

for T being complete LATTICE
for S being non empty full filtered-infs-inheriting SubRelStr of T holds incl (S,T) is filtered-infs-preserving