let L be non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr ; :: thesis: for x, y being Element of L holds x "|_|" y = x |_| y
let x, y be Element of L; :: thesis: x "|_|" y = x |_| y
x <= x "|_|" y by YELLOW_0:22;
then A1: x [= x "|_|" y by Th22;
y <= x "|_|" y by YELLOW_0:22;
then A2: y [= x "|_|" y by Th22;
x [= x |_| y by LATTICES:5;
then A3: x <= x |_| y by Th22;
y [= x |_| y by LATTICES:5;
then A4: y <= x |_| y by Th22;
(x |_| y) "|_|" (x "|_|" y) = ((x |_| y) "|_|" x) "|_|" y by LATTICE3:14
.= (x |_| y) "|_|" y by A3, YELLOW_0:24
.= x |_| y by A4, YELLOW_0:24 ;
then x "|_|" y <= x |_| y by YELLOW_0:24;
then A5: x "|_|" y [= x |_| y by Th22;
(x "|_|" y) |_| (x |_| y) = ((x "|_|" y) |_| x) |_| y by LATTICES:def 5
.= (x "|_|" y) |_| y by A1
.= x "|_|" y by A2 ;
hence x "|_|" y = x |_| y by A5; :: thesis: verum