let L be transitive antisymmetric with_suprema RelStr ; :: thesis: for S being non empty join-closed Subset of L holds subrelstr S is with_suprema

let S be non empty join-closed Subset of L; :: thesis: subrelstr S is with_suprema

subrelstr S is non empty full join-inheriting SubRelStr of L by Def2;

hence subrelstr S is with_suprema ; :: thesis: verum

let S be non empty join-closed Subset of L; :: thesis: subrelstr S is with_suprema

subrelstr S is non empty full join-inheriting SubRelStr of L by Def2;

hence subrelstr S is with_suprema ; :: thesis: verum