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

set x = the Element of IT;
take c = ((( the Element of IT `) `) "\/" ( the Element of IT `)) ` ; :: thesis:
let a be Element of IT; :: thesis:
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:
hence a "/\" c = c ; :: thesis:

end;