let S be 1-sorted ; :: thesis: for X, Y being Subset of holds
( X c= Y ` iff Y c= X ` )
let X, Y be Subset of ; :: thesis: ( X c= Y ` iff Y c= X ` )
Y = (Y ` ) ` ;
hence ( X c= Y ` iff Y c= X ` ) by SUBSET_1:31; :: thesis: verum