let L be non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr ; for x, y being Element of L holds x "|^|" y = x |^| y
let x, y be Element of L; x "|^|" y = x |^| y
x "|^|" y <= x
by YELLOW_0:23;
then A1:
x "|^|" y [= x
by Th22;
x "|^|" y <= y
by YELLOW_0:23;
then A2:
x "|^|" y [= y
by Th22;
x |^| y [= x
by LATTICES:6;
then A3:
x |^| y <= x
by Th22;
x |^| y [= y
by LATTICES:6;
then A4:
x |^| y <= y
by Th22;
(x |^| y) "|^|" (x "|^|" y) =
((x |^| y) "|^|" x) "|^|" y
by LATTICE3:16
.=
(x |^| y) "|^|" y
by A3, YELLOW_0:25
.=
x |^| y
by A4, YELLOW_0:25
;
then
x |^| y <= x "|^|" y
by YELLOW_0:25;
then A5:
x |^| y [= x "|^|" y
by Th22;
(x "|^|" y) |^| (x |^| y) =
((x "|^|" y) |^| x) |^| y
by LATTICES:def 7
.=
(x "|^|" y) |^| y
by A1, LATTICES:4
.=
x "|^|" y
by A2, LATTICES:4
;
hence
x "|^|" y = x |^| y
by A5, LATTICES:4; verum