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