theorem ProductIsSStone: :: LATSTONE:32

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