let A, B be complex-membered set ; :: thesis: A /// B = { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) }
thus A /// B c= { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } :: according to XBOOLE_0:def 10 :: thesis: { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } c= A /// B

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in A /// B or e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } )
assume e in A /// B ; :: thesis: e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) }
then consider c1, c2 being Element of COMPLEX such that
A1: e = c1 * c2 and
A2: c1 in A and
A3: c2 in B "" ;
A4: e = c1 / (c2 " ) by A1;
c2 " in B by A3, Th35;
hence e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } by A4, A2; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } or e in A /// B )
assume e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; :: thesis: e in A /// B
then consider c1, c2 being Element of COMPLEX such that
A5: e = c1 / c2 and
A6: c1 in A and
A7: c2 in B ;
c2 " in B "" by A7;
hence e in A /// B by A5, A6; :: thesis: verum