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 "\/" y ;
A2: ( y [= x "\/" y & y % = y ) by LATTICES:5;
A3: ( x [= x "\/" y & x % = x ) by LATTICES:5;
reconsider c = x "\/" y as Element of (LattPOSet L) ;
A4: b <= c by A1, A2, LATTICE3:7;
A5: 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 that
A6: a <= d and
A7: b <= d ; :: thesis: c <= d
reconsider z = d as Element of L ;
y % <= z % by A7;
then A8: y [= z by LATTICE3:7;
x % <= z % by A6;
then x [= z by LATTICE3:7;
then x "\/" y [= z by A8, FILTER_0:6;
then (x "\/" y) % <= z % by LATTICE3:7;
hence c <= d ; :: thesis: verum
end;
a <= c by A1, A3, LATTICE3:7;
hence a "\/" b = (% a) "\/" (% b) by A4, A5, YELLOW_0:22; :: thesis: verum