let L be non empty with_suprema with_infima PartialOrdered OrthoRelStr ; :: thesis: for x, y being Element of L st x <= y holds
( y = x "|_|" y & x = x "|^|" y )
let a, b be Element of L; :: thesis: ( a <= b implies ( b = a "|_|" b & a = a "|^|" b ) )
assume A1: a <= b ; :: thesis: ( b = a "|_|" b & a = a "|^|" b )
then b = b "|_|" a by YELLOW_0:24;
hence ( b = a "|_|" b & a = a "|^|" b ) by A1, LATTICE3:13, YELLOW_0:25; :: thesis: verum