:: deftheorem Def2 defines ^ POLNOT_1:def 2 :
for P, Q, b₃ being FinSequence-membered set holds
( b₃ = P ^ Q iff for a being object holds
( a in b₃ iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) ) );