let I be set ; :: thesis: for X being ManySortedSet of I holds
( X /\ ([[0]] I) = [[0]] I & ([[0]] I) /\ X = [[0]] I )
let X be ManySortedSet of I; :: thesis: ( X /\ ([[0]] I) = [[0]] I & ([[0]] I) /\ X = [[0]] I )
[[0]] I c= X by Th49;
hence ( X /\ ([[0]] I) = [[0]] I & ([[0]] I) /\ X = [[0]] I ) by Th25; :: thesis: verum