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

proof

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

end;

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