let n be non zero Nat; :: thesis: for a, b being Element of (Divisors_Lattice n) holds
( a "\/" b = a lcm b & a "/\" b = a gcd b )
let a, b be Element of (Divisors_Lattice n); :: thesis: ( a "\/" b = a lcm b & a "/\" b = a gcd b )
set L = Divisors_Lattice n;
set K = NatPlus_Lattice ;
A0: the carrier of (Divisors_Lattice n) c= the carrier of NatPlus_Lattice by NAT_LAT:def 12;
reconsider aa = a, bb = b as Element of NatPlus_Lattice by A0;
the L_join of (Divisors_Lattice n) = the L_join of NatPlus_Lattice || the carrier of (Divisors_Lattice n) by NAT_LAT:def 12;
hence a "\/" b = aa "\/" bb by FUNCT_1:49, ZFMISC_1:87
.= a lcm b ;
:: thesis: a "/\" b = a gcd b
the L_meet of (Divisors_Lattice n) = the L_meet of NatPlus_Lattice || the carrier of (Divisors_Lattice n) by NAT_LAT:def 12;
hence a "/\" b = aa "/\" bb by FUNCT_1:49, ZFMISC_1:87
.= a gcd b ;
:: thesis: verum