set SL = subrelstr ([#] L);
A1: the carrier of (subrelstr ([#] L)) = the carrier of L by YELLOW_0:def 15;
thus subrelstr ([#] L) is closure :: thesis: subrelstr ([#] L) is sups-inheriting

proof

let X be Subset of (subrelstr ([#] L)); :: according to YELLOW_0:def 18 :: thesis: ( not ex_inf_of X,L or "/\" X,L in the carrier of (subrelstr ([#] L)) )
thus ( not ex_inf_of X,L or "/\" X,L in the carrier of (subrelstr ([#] L)) ) by A1; :: thesis: verum

end;

let X be Subset of (subrelstr ([#] L)); :: according to YELLOW_0:def 19 :: thesis: ( not ex_sup_of X,L or "\/" X,L in the carrier of (subrelstr ([#] L)) )
thus ( not ex_sup_of X,L or "\/" X,L in the carrier of (subrelstr ([#] L)) ) by A1; :: thesis: verum