let E be set ; :: thesis: for A, B being Subset of E st A ` = B ` holds
A = B
let A, B be Subset of E; :: thesis: ( A ` = B ` implies A = B )
assume A ` = B ` ; :: thesis: A = B
hence A = (B `) `
.= B ;
:: thesis: verum