let A be non empty set ; :: thesis: for B being non empty trivial set st A c= B holds
A = B
let B be non empty trivial set ; :: thesis: ( A c= B implies A = B )
assume A1: A c= B ; :: thesis: A = B
consider s being Element of B such that
A2: B = {s} by Def1;
thus A = B by A1, A2, ZFMISC_1:39; :: thesis: verum