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