let L be D_Lattice; :: thesis: for a, b, c being Element of L st c "/\" a = c "/\" b & c "\/" a = c "\/" b holds
a = b
let a, b, c be Element of L; :: thesis: ( c "/\" a = c "/\" b & c "\/" a = c "\/" b implies a = b )
assume that
A1: c "/\" a = c "/\" b and
A2: c "\/" a = c "\/" b ; :: thesis: a = b
thus a = a "/\" (c "\/" a) by Def9
.= (b "/\" c) "\/" (b "/\" a) by A1, A2, Def11
.= b "/\" (c "\/" a) by Def11
.= b by A2, Def9 ; :: thesis: verum