thus [:A,B:] is Subset of [:X,Y:] by Def2; :: thesis: verum