theorem PsComplProduct: :: LATSTONE:30

for L1, L2 being Lattice st L1 is 01_Lattice & L2 is 01_Lattice holds
( ( L1 is pseudocomplemented & L2 is pseudocomplemented ) iff [:L1,L2:] is pseudocomplemented )