for x being object st x in rng <%S1%> holds
x is 1-sorted

proof

let x be object ; :: thesis: ( x in rng <%S1%> implies x is 1-sorted )
assume x in rng <%S1%> ; :: thesis: x is 1-sorted
then x in {S1} by AFINSQ_1:33;
hence x is 1-sorted by TARSKI:def 1; :: thesis: verum

end;

hence <%S1%> is 1-sorted-yielding ; :: thesis: verum