let IT be Ortholattice; :: thesis: IT is lower-bounded
ex c being Element of IT st
for a being Element of IT holds
( c "/\" a = c & a "/\" c = c )

proof

consider x being Element of IT;
take c = (((x ` ) ` ) "\/" (x ` )) ` ; :: 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 )
thus c "/\" a = ((((a ` ) ` ) "\/" (a ` )) ` ) "/\" a by ROBBINS3:def 7
.= ((a ` ) "/\" a) "/\" a by ROBBINS1:def 23
.= (a ` ) "/\" (a "/\" a) by LATTICES:def 7
.= (a ` ) "/\" a by LATTICES:18
.= (((a ` ) ` ) "\/" (a ` )) ` by ROBBINS1:def 23
.= c by ROBBINS3:def 7 ; :: thesis: a "/\" c = c
hence a "/\" c = c ; :: thesis: verum

end;

hence IT is lower-bounded by LATTICES:def 13; :: thesis: verum