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