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
ex s being Element of B st B = {s} by Def1;
hence A = B by A1, ZFMISC_1:39; :: thesis: verum