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