let D1, D2, D3 be non empty set ; 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 }
XBOOLE_0:def 10 { <*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
object ;
TARSKI:def 3 ( 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*>
;
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
object st
(
x in D1 &
y in D2 &
z in D3 &
a = <*x,y,z*> )
by Th123;
hence
a in { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum }
;
verum
end;
let a be object ; TARSKI:def 3 ( 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 }
; 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 Th123; verum