let a, b be Element of Nat_Lattice; :: thesis: ( a [= b implies a divides b )
assume a [= b ; :: thesis: a divides b
then a "\/" b = b by LATTICES:def 3;
hence a divides b by NEWTON:44; :: thesis: verum