let L be Lattice; for a, b being Element of L holds
( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) )
let a, b be Element of L; ( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) )
consider c being Element of L such that
A1:
c = a "/\" b
;
A2:
for d being Element of (LattPOSet L) st d <= a % & d <= b % holds
c % >= d
c [= b
by A1, LATTICES:6;
then A8:
c % <= b %
by LATTICE3:7;
c [= a
by A1, LATTICES:6;
then
c % <= a %
by LATTICE3:7;
then A9:
c % = (a %) "/\" (b %)
by A8, A2, YELLOW_0:23;
consider c being Element of L such that
A10:
c = a "\/" b
;
A11:
for d being Element of (LattPOSet L) st a % <= d & b % <= d holds
d >= c %
b [= c
by A10, LATTICES:5;
then A17:
b % <= c %
by LATTICE3:7;
a [= c
by A10, LATTICES:5;
then
a % <= c %
by LATTICE3:7;
then
c % = (a %) "\/" (b %)
by A17, A11, YELLOW_0:22;
hence
( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) )
by A1, A9, A10, LATTICE3:def 3; verum