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