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 Th7;
then A1: (b `) "/\" a [= Bottom L by Th18;
Bottom L [= (b `) "/\" a ;
then (b `) "/\" a = Bottom L by A1, Th6;
hence b ` [= a ` by Th23; :: thesis: verum