let B, A be set ; :: thesis: ( B c= A & A is trivial implies B is trivial )
assume that
A1: B c= A and
A2: 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 A1, TARSKI:def 3;
hence x = y by A2, Def10; :: thesis: verum