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 & x "/\" y [= y ) by LATTICES:23;
A2: ( (x "/\" y) % = x "/\" y & x % = x & y % = y & % ((x "/\" y) % ) = (x "/\" y) % & % (x % ) = x % & % (y % ) = y % ) ;
reconsider c = x "/\" y as Element of (LattPOSet L) ;
A3: ( c <= a & c <= b ) by A1, A2, LATTICE3:7;
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 )
assume A4: ( d <= a & d <= b ) ; :: thesis: d <= c
reconsider z = d as Element of L ;
A5: ( z % = z & % (z % ) = z % ) ;
then ( z [= x & z [= y ) by A2, A4, LATTICE3:7;
then z [= x "/\" y by FILTER_0:7;
hence d <= c by A2, A5, LATTICE3:7; :: thesis: verum

end;

hence a "/\" b = (% a) "/\" (% b) by A3, YELLOW_0:23; :: thesis: verum