dom (StoneH L) = the carrier of L by Def6;
hence not StoneS L is empty by RELAT_1:42; :: thesis: verum