let S be Subset of L; :: thesis: ( S is infs-closed implies S is meet-closed )
assume S is infs-closed ; :: thesis: S is meet-closed
then reconsider S1 = subrelstr S as infs-inheriting SubRelStr of L by Def3;
S1 is meet-inheriting ;
hence S is meet-closed by Def1; :: thesis: verum