let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y & X c= Z & Y misses Z holds
X = [0] I
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y & X c= Z & Y misses Z implies X = [0] I )
assume A1: ( X c= Y & X c= Z ) ; :: thesis: ( not Y misses Z or X = [0] I )
assume Y misses Z ; :: thesis: X = [0] I
then Y /\ Z = [0] I by Th121;
hence X = [0] I by A1, Th19, Th50; :: thesis: verum