let L be lower-bounded pseudocomplemented Lattice; :: thesis: for a, b, x being Element of L st a is_a_pseudocomplement_of x & b is_a_pseudocomplement_of x holds
a = b
let a, b, x be Element of L; :: thesis: ( a is_a_pseudocomplement_of x & b is_a_pseudocomplement_of x implies a = b )
assume that
a1: a is_a_pseudocomplement_of x and
b1: b is_a_pseudocomplement_of x ; :: thesis: a = b
a2: a "/\" x = Bottom L by a1;
b2: b "/\" x = Bottom L by b1;
ab1: b [= a by a1, b2;
a [= b by b1, a2;
hence a = b by ab1, LATTICES:8; :: thesis: verum