let f be Function; :: thesis: ( f is PLS-yielding implies ( f is non-Empty & f is TopStruct-yielding ) )
assume A1: f is PLS-yielding ; :: thesis: ( f is non-Empty & f is TopStruct-yielding )
thus f is non-Empty :: thesis: f is TopStruct-yielding

proof

let S be 1-sorted ; :: according to WAYBEL_3:def 7 :: thesis: ( not S in rng f or not S is empty )
assume S in rng f ; :: thesis: not S is empty
hence not S is empty by A1, Def19; :: thesis: verum

end;

let x be set ; :: according to PENCIL_1:def 13 :: thesis: ( x in rng f implies x is TopStruct )
assume x in rng f ; :: thesis: x is TopStruct
hence x is TopStruct by A1, Def19; :: thesis: verum