let I be set ; :: thesis: for M being non-empty ManySortedSet of I
for X, Y being Element of M st X c= Y holds
(id M) .. X c= (id M) .. Y
let M be non-empty ManySortedSet of I; :: thesis: for X, Y being Element of M st X c= Y holds
(id M) .. X c= (id M) .. Y
let X, Y be Element of M; :: thesis: ( X c= Y implies (id M) .. X c= (id M) .. Y )
assume A1: X c= Y ; :: thesis: (id M) .. X c= (id M) .. Y
(id M) .. X = X by Th8;
hence (id M) .. X c= (id M) .. Y by A1, Th8; :: thesis: verum