let L be B_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 (b `) "/\" a [= (b `) "/\" b by Th27;
then A1: (b `) "/\" a [= Bottom L by Th47;
Bottom L [= (b `) "/\" a by Th41;
then (b `) "/\" a = Bottom L by A1, Th26;
hence b ` [= a ` by Th52; :: thesis: verum