let D1, D2 be non empty set ; :: thesis: product <*D1,D2*> = { <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum }
thus product <*D1,D2*> c= { <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum } :: according to XBOOLE_0:def 10 :: thesis: { <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum } c= product <*D1,D2*>
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in product <*D1,D2*> or a in { <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum } )
assume a in product <*D1,D2*> ; :: thesis: a in { <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum }
then ex x, y being object st
( x in D1 & y in D2 & a = <*x,y*> ) by Th122;
hence a in { <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum } ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum } or a in product <*D1,D2*> )
assume a in { <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum } ; :: thesis: a in product <*D1,D2*>
then ex d1 being Element of D1 ex d2 being Element of D2 st a = <*d1,d2*> ;
hence a in product <*D1,D2*> by Th122; :: thesis: verum