let S be Subset of L; :: thesis: ( S is sups-closed implies S is join-closed )
assume S is sups-closed ; :: thesis: S is join-closed
then reconsider S1 = subrelstr S as sups-inheriting SubRelStr of L by Def4;
S1 is join-inheriting ;
hence S is join-closed by Def2; :: thesis: verum