let L1, L2 be Lattice; :: thesis: for p1, q1 being Element of L1

for p2, q2 being Element of L2 holds

( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )

let p1, q1 be Element of L1; :: thesis: for p2, q2 being Element of L2 holds

( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )

let p2, q2 be Element of L2; :: thesis: ( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )

thus ( [p1,p2] [= [q1,q2] implies ( p1 [= q1 & p2 [= q2 ) ) :: thesis: ( p1 [= q1 & p2 [= q2 implies [p1,p2] [= [q1,q2] )

A1: p1 "\/" q1 = q1 and

A2: p2 "\/" q2 = q2 ; :: according to LATTICES:def 3 :: thesis: [p1,p2] [= [q1,q2]

thus [p1,p2] "\/" [q1,q2] = [q1,q2] by A1, A2, Th21; :: according to LATTICES:def 3 :: thesis: verum

for p2, q2 being Element of L2 holds

( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )

let p1, q1 be Element of L1; :: thesis: for p2, q2 being Element of L2 holds

( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )

let p2, q2 be Element of L2; :: thesis: ( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )

thus ( [p1,p2] [= [q1,q2] implies ( p1 [= q1 & p2 [= q2 ) ) :: thesis: ( p1 [= q1 & p2 [= q2 implies [p1,p2] [= [q1,q2] )

proof

assume that
assume
[p1,p2] "\/" [q1,q2] = [q1,q2]
; :: according to LATTICES:def 3 :: thesis: ( p1 [= q1 & p2 [= q2 )

then [(p1 "\/" q1),(p2 "\/" q2)] = [q1,q2] by Th21;

hence ( p1 "\/" q1 = q1 & p2 "\/" q2 = q2 ) by XTUPLE_0:1; :: according to LATTICES:def 3 :: thesis: verum

end;then [(p1 "\/" q1),(p2 "\/" q2)] = [q1,q2] by Th21;

hence ( p1 "\/" q1 = q1 & p2 "\/" q2 = q2 ) by XTUPLE_0:1; :: according to LATTICES:def 3 :: thesis: verum

A1: p1 "\/" q1 = q1 and

A2: p2 "\/" q2 = q2 ; :: according to LATTICES:def 3 :: thesis: [p1,p2] [= [q1,q2]

thus [p1,p2] "\/" [q1,q2] = [q1,q2] by A1, A2, Th21; :: according to LATTICES:def 3 :: thesis: verum