let L be transitive antisymmetric with_infima RelStr ; :: thesis: for S being non empty meet-closed Subset of L holds subrelstr S is with_infima
let S be non empty meet-closed Subset of L; :: thesis: subrelstr S is with_infima
subrelstr S is non empty full meet-inheriting SubRelStr of L by Def1;
hence subrelstr S is with_infima ; :: thesis: verum