let L be Lattice; :: thesis: for a, b being Element of (LattPOSet L) holds a "/\" b = (% a) "/\" (% b)
let a, b be Element of (LattPOSet L); :: thesis: 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

proof

let d be Element of (LattPOSet L); :: thesis: ( d <= a & d <= b implies d <= c )
reconsider z = d as Element of L ;
A8: z % = z ;
assume ( d <= a & d <= b ) ; :: thesis: d <= c
then ( z [= x & z [= y ) by A6, A4, A8, LATTICE3:7;
then z [= x "/\" y by FILTER_0:7;
hence d <= c by A3, A8, LATTICE3:7; :: thesis: verum

end;

c <= a by A1, A3, A6, LATTICE3:7;
hence a "/\" b = (% a) "/\" (% b) by A5, A7, YELLOW_0:23; :: thesis: verum