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

.= (b "/\" x) "\/" (b "/\" a) by A1

.= (x "/\" b) "\/" (b "/\" a) by A1

.= (x "/\" b) "\/" (a "/\" b) by A1

.= (Bot' L) "\/" (a "/\" b) by A3

.= (a "/\" x) "\/" (a "/\" b) by A2

.= a "/\" (x "\/" b) by A1

.= a "/\" (Top' L) by A3

.= a by A1, Def2 ;

hence a = b ; :: thesis: verum

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

.= (b "/\" x) "\/" (b "/\" a) by A1

.= (x "/\" b) "\/" (b "/\" a) by A1

.= (x "/\" b) "\/" (a "/\" b) by A1

.= (Bot' L) "\/" (a "/\" b) by A3

.= (a "/\" x) "\/" (a "/\" b) by A2

.= a "/\" (x "\/" b) by A1

.= a "/\" (Top' L) by A3

.= a by A1, Def2 ;

hence a = b ; :: thesis: verum