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 Th12;
hence B ` c= A ; :: thesis: verum