let f be TopStruct-yielding Function; :: thesis: ( f is PLS-yielding implies f is non-void-yielding )
assume A2: f is PLS-yielding ; :: thesis: f is non-void-yielding
let x be set ; :: according to PENCIL_1:def 15 :: thesis: ( x in rng f implies x is non void TopStruct )
assume x in rng f ; :: thesis: x is non void TopStruct
hence x is non void TopStruct by A2, Def19; :: thesis: verum