let I be set ; :: thesis: for X being ManySortedSet of I holds
( X \+\ ([[0]] I) = X & ([[0]] I) \+\ X = X )
let X be ManySortedSet of I; :: thesis: ( X \+\ ([[0]] I) = X & ([[0]] I) \+\ X = X )
thus X \+\ ([[0]] I) = X \/ (([[0]] I) \ X) by Th65
.= X \/ ([[0]] I) by Th66
.= X by Th53 ; :: thesis: ([[0]] I) \+\ X = X
thus ([[0]] I) \+\ X = ([[0]] I) \/ (X \ ([[0]] I)) by Th66
.= ([[0]] I) \/ X by Th65
.= X by Th53 ; :: thesis: verum