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 Th9;
then A1: (b `) "/\" a [= Bottom L by Th20;
Bottom L [= (b `) "/\" a by Th16;
then (b `) "/\" a = Bottom L by A1, Th8;
hence b ` [= a ` by Th25; :: thesis: verum