let x be Element of [:X1,X2:]; :: thesis: x is pair
ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2] by Lm1;
hence x is pair ; :: thesis: verum