let A, B 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 object ; :: according to ZFMISC_1:def 10 :: thesis: for y being object st x in B & y in B holds
x = y
let y be object ; :: 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;
hence x = y by A2; :: thesis: verum