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

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 )
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
.= (((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 ; :: thesis: verum