let B, A be set ; :: thesis: ( B c= A & A is trivial implies B is trivial )
assume that
Z1: B c= A and
Z2: A is trivial ; :: thesis: B is trivial
let x be set ; :: according to ZFMISC_1:def 10 :: thesis: for y being set st x in B & y in B holds
x = y
let y be set ; :: thesis: ( x in B & y in B implies x = y )
assume ( x in B & y in B ) ; :: thesis: x = y
then ( x in A & y in A ) by Z1, TARSKI:def 3;
hence x = y by Z2, Def10; :: thesis: verum