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
A4: ( x "\/" b = Top L & x "/\" b = Bottom L ) by A3, Def18;
( x "\/" a = Top L & x "/\" a = Bottom L ) by A2, Def18;
hence a = b by A1, A4, Th32; :: thesis: verum