let X, Y be set ; :: thesis: for D being Subset of [:X,Y:] holds D c= [:(proj1 D),(proj2 D):]
let D be Subset of [:X,Y:]; :: thesis: D c= [:(proj1 D),(proj2 D):]
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in D or q in [:(proj1 D),(proj2 D):] )
assume A1: q in D ; :: thesis: q in [:(proj1 D),(proj2 D):]
then consider x, y being object such that
x in X and
y in Y and
A2: q = [x,y] by ZFMISC_1:def 2;
( x in proj1 D & y in proj2 D ) by A1, A2, XTUPLE_0:def 12, XTUPLE_0:def 13;
hence q in [:(proj1 D),(proj2 D):] by A2, ZFMISC_1:def 2; :: thesis: verum