let L1, L2 be Lattice; :: thesis: ( L1 is pseudocomplemented satisfying_Stone_identity 01_Lattice & L2 is pseudocomplemented satisfying_Stone_identity 01_Lattice implies [:L1,L2:] is satisfying_Stone_identity )
assume that
A1: L1 is pseudocomplemented satisfying_Stone_identity 01_Lattice and
A2: L2 is pseudocomplemented satisfying_Stone_identity 01_Lattice ; :: thesis: [:L1,L2:] is satisfying_Stone_identity
set L = [:L1,L2:];
for x being Element of [:L1,L2:] holds (x *) "\/" ((x *) *) = Top [:L1,L2:]

proof

let x be Element of [:L1,L2:]; :: thesis: (x *) "\/" ((x *) *) = Top [:L1,L2:]
consider x1, x2 being object such that
A3: ( x1 in the carrier of L1 & x2 in the carrier of L2 & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1 as Element of L1 by A3;
reconsider x2 = x2 as Element of L2 by A3;
X1: [(x1 *),(x2 *)] = x * by ProductPCompl, A3, A1, A2;
A4: (x1 *) "\/" ((x1 *) *) = Top L1 by A1, SatStone;
[((x1 *) "\/" ((x1 *) *)),((x2 *) "\/" ((x2 *) *))] = [(Top L1),(Top L2)] by A4, A2, SatStone
.= Top [:L1,L2:] by FILTER_1:43, A1, A2 ;
then Top [:L1,L2:] = [(x1 *),(x2 *)] "\/" [((x1 *) *),((x2 *) *)] by FILTER_1:35
.= (x *) "\/" ((x *) *) by X1, ProductPCompl, A1, A2 ;
hence (x *) "\/" ((x *) *) = Top [:L1,L2:] ; :: thesis: verum

end;

hence [:L1,L2:] is satisfying_Stone_identity ; :: thesis: verum