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