theorem ThProdPoset01: :: POSET_2:4

for P, Q being non empty RelStr
for x being object holds
( x is Element of [:P,Q:] iff ex p being Element of P ex q being Element of Q st x = [p,q] )