let L1, L2 be 1_Lattice; :: thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies Top L1 = Top L2 )
assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; :: thesis: Top L1 = Top L2
then reconsider c = Top L1 as Element of L2 ;

now :: thesis: for a being Element of L2 holds
( c "\/" a = c & a "\/" c = c )

let a be Element of L2; :: thesis: ( c "\/" a = c & a "\/" c = c )
reconsider b = a as Element of L1 by A1;
(Top L1) "\/" b = Top L1 ;
hence c "\/" a = c by A1; :: thesis: a "\/" c = c
hence a "\/" c = c ; :: thesis: verum

end;

hence Top L1 = Top L2 by LATTICES:def 17; :: thesis: verum