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 [= x "\/" y & y [= x "\/" y ) by LATTICES:22;
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: ( a <= c & b <= c ) by A1, A2, LATTICE3:7;
for d being Element of (LattPOSet L) st a <= d & b <= d holds
c <= d

proof

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

end;

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