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 )

ex c being Element of IT st

for a being Element of IT holds

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

proof

hence
IT is lower-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 )

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;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