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 )

proof

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;

hence IT is upper-bounded ; :: thesis: verum