let IT be Ortholattice; :: thesis: IT is upper-bounded

ex c being Element of IT st

for a being Element of IT holds

( c "\/" a = c & a "\/" c = c )

ex c being Element of IT st

for a being Element of IT holds

( c "\/" a = c & a "\/" c = c )

proof

hence
IT is upper-bounded
; :: thesis: verum
set x = the Element of IT;

take c = ( the Element of IT `) "\/" the Element of IT; :: thesis: for a being Element of IT holds

( c "\/" a = c & a "\/" c = c )

let a be Element of IT; :: thesis: ( c "\/" a = c & a "\/" c = c )

c "\/" a = ((a `) "\/" a) "\/" a by ROBBINS3:def 7

.= (a `) "\/" (a "\/" a) by LATTICES:def 5

.= (a `) "\/" a

.= c by ROBBINS3:def 7 ;

hence ( c "\/" a = c & a "\/" c = c ) ; :: thesis: verum

end;take c = ( the Element of IT `) "\/" the Element of IT; :: thesis: for a being Element of IT holds

( c "\/" a = c & a "\/" c = c )

let a be Element of IT; :: thesis: ( c "\/" a = c & a "\/" c = c )

c "\/" a = ((a `) "\/" a) "\/" a by ROBBINS3:def 7

.= (a `) "\/" (a "\/" a) by LATTICES:def 5

.= (a `) "\/" a

.= c by ROBBINS3:def 7 ;

hence ( c "\/" a = c & a "\/" c = c ) ; :: thesis: verum