let n be non zero square-free Nat; :: thesis: Divisors_Lattice n is Boolean
set L = Divisors_Lattice n;
Divisors_Lattice n is complemented

proof

for b being Element of (Divisors_Lattice n) ex a being Element of (Divisors_Lattice n) st a is_a_complement_of b

proof

let b be Element of (Divisors_Lattice n); :: thesis: ex a being Element of (Divisors_Lattice n) st a is_a_complement_of b
b in the carrier of (Divisors_Lattice n) ;
then aa: b in NatDivisors n by DivLat;
then A1: n = b * (n div b) by NAT_D:3, MOEBIUS1:39;
set a = n div b;
n div b <> 0 by DivNonZero, aa, MOEBIUS1:39;
then n div b in NatDivisors n by MOEBIUS1:39, A1, NAT_D:def 3;
then reconsider a = n div b as Element of (Divisors_Lattice n) by DivLat;
take a ; :: thesis: a is_a_complement_of b
reconsider aa = a, bb = b as non zero Element of NAT by DivNonZero, aa, MOEBIUS1:39;
S1: aa,bb are_coprime by aa, MOEBIUS1:39, DivRelPrime;
then a lcm b = n by A1, INT615;
hence a is_a_complement_of b by S1, TopBot; :: thesis: verum

end;

hence Divisors_Lattice n is complemented ; :: thesis: verum

end;

hence Divisors_Lattice n is Boolean ; :: thesis: verum