let E be set ; :: thesis: for A, B being Subset of E holds
( A c= B iff B ` c= A ` )
let A, B be Subset of E; :: thesis: ( A c= B iff B ` c= A ` )
thus ( A c= B implies B ` c= A ` ) by XBOOLE_1:34; :: thesis: ( B ` c= A ` implies A c= B )
A1: E \ (B `) = (B `) `
.= B ;
E \ (A `) = (A `) `
.= A ;
hence ( B ` c= A ` implies A c= B ) by A1, XBOOLE_1:34; :: thesis: verum