let L1, L2 be Lattice; :: thesis: ( L1 is 0_Lattice & L2 is 0_Lattice implies Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)] )

assume that

A1: L1 is 0_Lattice and

A2: L2 is 0_Lattice ; :: thesis: Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)]

hence Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)] by A3, LATTICES:def 16; :: thesis: verum

assume that

A1: L1 is 0_Lattice and

A2: L2 is 0_Lattice ; :: thesis: Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)]

A3: now :: thesis: for a being Element of [:L1,L2:] holds

( [(Bottom L1),(Bottom L2)] "/\" a = [(Bottom L1),(Bottom L2)] & a "/\" [(Bottom L1),(Bottom L2)] = [(Bottom L1),(Bottom L2)] )

[:L1,L2:] is lower-bounded
by A1, A2, Th39;( [(Bottom L1),(Bottom L2)] "/\" a = [(Bottom L1),(Bottom L2)] & a "/\" [(Bottom L1),(Bottom L2)] = [(Bottom L1),(Bottom L2)] )

let a be Element of [:L1,L2:]; :: thesis: ( [(Bottom L1),(Bottom L2)] "/\" a = [(Bottom L1),(Bottom L2)] & a "/\" [(Bottom L1),(Bottom L2)] = [(Bottom L1),(Bottom L2)] )

consider p1 being Element of L1, p2 being Element of L2 such that

A4: a = [p1,p2] by DOMAIN_1:1;

thus [(Bottom L1),(Bottom L2)] "/\" a = [((Bottom L1) "/\" p1),((Bottom L2) "/\" p2)] by A4, Th21

.= [(Bottom L1),((Bottom L2) "/\" p2)] by A1

.= [(Bottom L1),(Bottom L2)] by A2 ; :: thesis: a "/\" [(Bottom L1),(Bottom L2)] = [(Bottom L1),(Bottom L2)]

hence a "/\" [(Bottom L1),(Bottom L2)] = [(Bottom L1),(Bottom L2)] ; :: thesis: verum

end;consider p1 being Element of L1, p2 being Element of L2 such that

A4: a = [p1,p2] by DOMAIN_1:1;

thus [(Bottom L1),(Bottom L2)] "/\" a = [((Bottom L1) "/\" p1),((Bottom L2) "/\" p2)] by A4, Th21

.= [(Bottom L1),((Bottom L2) "/\" p2)] by A1

.= [(Bottom L1),(Bottom L2)] by A2 ; :: thesis: a "/\" [(Bottom L1),(Bottom L2)] = [(Bottom L1),(Bottom L2)]

hence a "/\" [(Bottom L1),(Bottom L2)] = [(Bottom L1),(Bottom L2)] ; :: thesis: verum

hence Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)] by A3, LATTICES:def 16; :: thesis: verum