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

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