let n be non zero Nat; :: thesis: ( Divisors_Lattice n is Boolean iff n is square-free )
set L = Divisors_Lattice n;
thus ( Divisors_Lattice n is Boolean implies n is square-free ) :: thesis: ( n is square-free implies Divisors_Lattice n is Boolean )

proof

assume A0: Divisors_Lattice n is Boolean ; :: thesis: n is square-free
assume n is square-containing ; :: thesis: contradiction
then consider p being Prime such that
A1: p |^ 2 divides n by MOEBIUS1:def 1;
a1: p * p divides n by A1, NEWTON:81;
A2: p <> 1 by INT_2:def 4;
p divides p * p ;
then p divides p |^ 2 by NEWTON:81;
then p in NatDivisors n by MOEBIUS1:39, A1, NAT_D:4;
then reconsider pp = p as Element of (Divisors_Lattice n) by DivLat;
for a being Element of (Divisors_Lattice n) holds not a is_a_complement_of pp

proof

given a being Element of (Divisors_Lattice n) such that C1: a is_a_complement_of pp ; :: thesis: contradiction
C2: ( a lcm p = n & a gcd p = 1 ) by C1, TopBot;
a,p are_coprime by C1, TopBot;
then a lcm p = a * p by INT615;
then p divides a by C2, a1, INT_4:7;
then p divides a gcd p by NAT_D:def 5;
then C5: p <= a gcd p by NAT_D:7;
a gcd p <> 1

proof

assume a gcd p = 1 ; :: thesis: contradiction
then p < 1 + 1 by C5, NAT_1:13;
hence contradiction by A2, NAT_1:23; :: thesis: verum

end;

hence contradiction by C1, TopBot; :: thesis: verum

end;

hence contradiction by A0, LATTICES:def 19; :: thesis: verum

end;

thus ( n is square-free implies Divisors_Lattice n is Boolean ) ; :: thesis: verum