let L be Lattice; for a, b being Element of (LattPOSet L) holds a "/\" b = (% a) "/\" (% b)
let a, b be Element of (LattPOSet L); a "/\" b = (% a) "/\" (% b)
reconsider x = a, y = b as Element of L ;
set c = x "/\" y;
A1:
x "/\" y [= x
by LATTICES:6;
A2:
x "/\" y [= y
by LATTICES:6;
A3:
(x "/\" y) % = x "/\" y
;
reconsider c = x "/\" y as Element of (LattPOSet L) ;
A4:
y % = y
;
then A5:
c <= b
by A2, A3, LATTICE3:7;
A6:
x % = x
;
A7:
for d being Element of (LattPOSet L) st d <= a & d <= b holds
d <= c
c <= a
by A1, A3, A6, LATTICE3:7;
hence
a "/\" b = (% a) "/\" (% b)
by A5, A7, YELLOW_0:23; verum