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

proof

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

end;

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