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:12; :: thesis: verum