let L be lower-bounded pseudocomplemented Lattice; :: thesis: for a, b being Element of L st a [= b holds
b * [= a *
let a, b be Element of L; :: thesis: ( a [= b implies b * [= a * )
assume a [= b ; :: thesis: b * [= a *
then a1: a "/\" b = a by LATTICES:4;
a2: a * is_a_pseudocomplement_of a by def3;
a "/\" (b *) = ((b *) "/\" b) "/\" a by a1, LATTICES:def 7
.= (Bottom L) "/\" a by ThD
.= Bottom L ;
hence b * [= a * by a2; :: thesis: verum