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