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