let f be TopStruct-yielding Function; :: thesis: ( f is PLS-yielding implies f is non-Trivial-yielding )
assume A1: f is PLS-yielding ; :: thesis: f is non-Trivial-yielding
let x be set ; :: according to PENCIL_1:def 18 :: thesis: ( x in rng f implies x is non trivial 1-sorted )
assume x in rng f ; :: thesis: x is non trivial 1-sorted
then reconsider S1 = x as non empty non void with_non_trivial_blocks TopStruct by A1;
consider s being object such that
A2: s in the topology of S1 by XBOOLE_0:def 1;
reconsider s = s as Block of S1 by A2;
2 c= card s by Def6;
then ex s1, s2 being object st
( s1 in s & s2 in s & s1 <> s2 ) by Th2;
hence x is non trivial 1-sorted by A2, STRUCT_0:def 10; :: thesis: verum