let L1, L2 be Lattice; :: thesis: ( L1 is 1_Lattice & L2 is 1_Lattice implies Top [:L1,L2:] = [(Top L1),(Top L2)] )
assume that
A1: L1 is 1_Lattice and
A2: L2 is 1_Lattice ; :: thesis: Top [:L1,L2:] = [(Top L1),(Top L2)]

A3: now :: thesis: for a being Element of [:L1,L2:] holds
( [(Top L1),(Top L2)] "\/" a = [(Top L1),(Top L2)] & a "\/" [(Top L1),(Top L2)] = [(Top L1),(Top L2)] )

let a be Element of [:L1,L2:]; :: thesis: ( [(Top L1),(Top L2)] "\/" a = [(Top L1),(Top L2)] & a "\/" [(Top L1),(Top L2)] = [(Top L1),(Top L2)] )
consider p1 being Element of L1, p2 being Element of L2 such that
A4: a = [p1,p2] by DOMAIN_1:1;
thus [(Top L1),(Top L2)] "\/" a = [((Top L1) "\/" p1),((Top L2) "\/" p2)] by A4, Th21
.= [(Top L1),((Top L2) "\/" p2)] by A1
.= [(Top L1),(Top L2)] by A2 ; :: thesis: a "\/" [(Top L1),(Top L2)] = [(Top L1),(Top L2)]
hence a "\/" [(Top L1),(Top L2)] = [(Top L1),(Top L2)] ; :: thesis: verum

end;

[:L1,L2:] is upper-bounded by A1, A2, Th40;
hence Top [:L1,L2:] = [(Top L1),(Top L2)] by A3, LATTICES:def 17; :: thesis: verum