let a, b be Element of L; :: thesis: ( a is_a_complement'_of x & b is_a_complement'_of x implies a = b )
assume that
A2: a is_a_complement'_of x and
A3: b is_a_complement'_of x ; :: thesis: a = b
b = b "/\" (Top' L) by A1, Def2
.= b "/\" (x "\/" a) by A2, Def6
.= (b "/\" x) "\/" (b "/\" a) by A1, LATTICES:def 11
.= (x "/\" b) "\/" (b "/\" a) by A1, LATTICES:def 6
.= (x "/\" b) "\/" (a "/\" b) by A1, LATTICES:def 6
.= (Bot' L) "\/" (a "/\" b) by A3, Def6
.= (a "/\" x) "\/" (a "/\" b) by A2, Def6
.= a "/\" (x "\/" b) by A1, LATTICES:def 11
.= a "/\" (Top' L) by A3, Def6
.= a by A1, Def2 ;
hence a = b ; :: thesis: verum