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 FINSEQ_2:128;
hence x is 1-sorted by ENUMSET1:def 1; :: thesis: verum

end;

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