let n be non zero Nat; :: thesis: ( Top (Divisors_Lattice n) = n & Bottom (Divisors_Lattice n) = 1 )
set L = Divisors_Lattice n;
n in NatDivisors n by MOEBIUS1:39;
then reconsider TT = n as Element of (Divisors_Lattice n) by DivLat;
a1: for a being Element of (Divisors_Lattice n) holds
( TT "\/" a = TT & a "\/" TT = TT )
proof
let a be Element of (Divisors_Lattice n); :: thesis: ( TT "\/" a = TT & a "\/" TT = TT )
a in the carrier of (Divisors_Lattice n) ;
then a in NatDivisors n by DivLat;
hence ( TT "\/" a = TT & a "\/" TT = TT ) by NEWTON:44, MOEBIUS1:39; :: thesis: verum
end;
1 in NatDivisors n by MOEBIUS1:39, NAT_D:6;
then reconsider TT = 1 as Element of (Divisors_Lattice n) by DivLat;
for a being Element of (Divisors_Lattice n) holds
( TT "/\" a = TT & a "/\" TT = TT ) by NEWTON:51;
hence ( Top (Divisors_Lattice n) = n & Bottom (Divisors_Lattice n) = 1 ) by a1, LATTICES:def 16, LATTICES:def 17; :: thesis: verum