let c1, c2 be Element of L; :: thesis: ( ( for a being Element of L holds
( c1 "/\" a = a & a "/\" c1 = a ) ) & ( for a being Element of L holds
( c2 "/\" a = a & a "/\" c2 = a ) ) implies c1 = c2 )
assume that
A2: for a being Element of L holds
( c1 "/\" a = a & a "/\" c1 = a ) and
A3: for a being Element of L holds
( c2 "/\" a = a & a "/\" c2 = a ) ; :: thesis: c1 = c2
thus c1 = c2 "/\" c1 by A3
.= c2 by A2 ; :: thesis: verum