let f be TopStruct-yielding Function; :: thesis: ( f is PLS-yielding implies f is non-Trivial-yielding )
assume A3: 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 A3, Def19;
consider s being set such that
A4: s in the topology of S1 by XBOOLE_0:def 1;
reconsider s = s as Block of S1 by A4;
2 c= card s by Def6;
then ex s1, s2 being set st
( s1 in s & s2 in s & s1 <> s2 ) by Th2;
hence x is non trivial 1-sorted by A4, STRUCT_0:def 10; :: thesis: verum