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