let L1, L2 be strict SubLattice of NatPlus_Lattice ; :: thesis: ( the carrier of L1 = NatDivisors n & the carrier of L2 = NatDivisors n implies L1 = L2 )
assume that
A1: the carrier of L1 = NatDivisors n and
A2: the carrier of L2 = NatDivisors n ; :: thesis: L1 = L2
set L = NatPlus_Lattice ;
A3: the L_meet of L1 = the L_meet of NatPlus_Lattice || the carrier of L1 by NAT_LAT:def 12
.= the L_meet of L2 by NAT_LAT:def 12, A1, A2 ;
the L_join of L1 = the L_join of NatPlus_Lattice || the carrier of L1 by NAT_LAT:def 12
.= the L_join of L2 by NAT_LAT:def 12, A1, A2 ;
hence L1 = L2 by A3, A1, A2; :: thesis: verum