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