set SL = subrelstr ([#] L);
A1: the carrier of (subrelstr ([#] L)) = the carrier of L by YELLOW_0:def 15;
thus subrelstr ([#] L) is infs-inheriting by A1; :: thesis: subrelstr ([#] L) is sups-inheriting
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