let A be non empty set ; :: thesis: for B being 1 -element set st A c= B holds
A = B
let B be 1 -element 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 SUBSET_1:46;
hence A = B by A1, ZFMISC_1:33; :: thesis: verum