consider x being set such that
A1: x in E by XBOOLE_0:def 1;
take {x} ; :: thesis: ( {x} is Subset of E & not {x} is empty & {x} is trivial )
thus ( {x} is Subset of E & not {x} is empty & {x} is trivial ) by A1, REALSET1:def 4, ZFMISC_1:37; :: thesis: verum