A1: rng (X --> S) c= {S} by FUNCOP_1:19;
let x be set ; :: according to YELLOW16:def 5 :: thesis: ( x in rng (X --> S) implies x is Poset )
assume x in rng (X --> S) ; :: thesis: x is Poset
hence x is Poset by A1, TARSKI:def 1; :: thesis: verum