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

( 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