let b1, b2 be Element of L; :: thesis: ( ( for a being Element of L holds b1 "/\" a = b1 ) & ( for a being Element of L holds b2 "/\" a = b2 ) implies b1 = b2 )
assume that
A2: for a being Element of L holds b1 "/\" a = b1 and
A3: for a being Element of L holds b2 "/\" a = b2 ; :: thesis: b1 = b2
A4: b1 "/\" b2 = b1 by A2;
A5: b2 "/\" b1 = b2 by A3;
(b1 "/\" b2) "/\" b1 = b1 "/\" (b2 "/\" b1) by LATTICES:def 7
.= b1 "/\" b2 by A3 ;
then b1 "/\" b2 [= b1 by LATTICES:def 8;
hence b1 = b2 by A4, A5, Th3715; :: thesis: verum