theorem ProductPCompl: :: LATSTONE:31

for L1, L2 being Lattice
for p1 being Element of L1
for p2 being Element of L2 st L1 is pseudocomplemented 01_Lattice & L2 is pseudocomplemented 01_Lattice holds
[p1,p2] * = [(p1 *),(p2 *)]