let X1, X2 be set ; :: thesis: ( X1 <> {} & X2 <> {} implies for x being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2] )
assume A1: ( X1 <> {} & X2 <> {} ) ; :: thesis: for x being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2]
let x be Element of [:X1,X2:]; :: thesis: ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2]
reconsider xx2 = x `2 as Element of X2 by A1, Th4;
reconsider xx1 = x `1 as Element of X1 by A1, Th4;
take xx1 ; :: thesis: ex xx2 being Element of X2 st x = [xx1,xx2]
take xx2 ; :: thesis: x = [xx1,xx2]
thus x = [xx1,xx2] by A1, Th15; :: thesis: verum