thus O1 \ O2 is Subset of [:X,X:] ; :: thesis: verum