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