consider A9, B9 being Subset of X such that
A1: A = [A9,B9] by Th55;
thus A `1 is Subset of X by A1; :: thesis: verum