let D1, D2, D3 be non empty set ; :: thesis: product <*D1,D2,D3*> = { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum }
thus product <*D1,D2,D3*> c= { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum } :: according to XBOOLE_0:def 10 :: thesis: { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum } c= product <*D1,D2,D3*>

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in product <*D1,D2,D3*> or a in { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum } )
assume a in product <*D1,D2,D3*> ; :: thesis: a in { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum }
then ex x, y, z being set st
( x in D1 & y in D2 & z in D3 & a = <*x,y,z*> ) by Th3;
hence a in { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum } ; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum } or a in product <*D1,D2,D3*> )
assume a in { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum } ; :: thesis: a in product <*D1,D2,D3*>
then ex d1 being Element of D1 ex d2 being Element of D2 ex d3 being Element of D3 st a = <*d1,d2,d3*> ;
hence a in product <*D1,D2,D3*> by Th3; :: thesis: verum