deffunc H₂( object ) -> set = {I};
consider S being ManySortedSet of I such that
A1: for x being object st x in I holds
S . x = H₂(x) from PBOOLE:sch 4();
take S ; :: thesis: ( S is non-empty & S is trivial-yielding )

hereby :: according to PBOOLE:def 13 :: thesis: S is trivial-yielding

let x be object ; :: thesis: ( x in I implies not S . x is empty )
assume x in I ; :: thesis: not S . x is empty
then S . x = H₂(x) by A1;
hence not S . x is empty ; :: thesis: verum

end;

let x be set ; :: according to MSAFREE4:def 2 :: thesis: ( x in I implies S . x is trivial )
assume x in I ; :: thesis: S . x is trivial
then S . x = H₂(x) by A1;
hence S . x is trivial ; :: thesis: verum