let L be non empty Boolean RelStr ; :: thesis: for a, b being Element of L st a <= b \ a holds
a = Bottom L
let a, b be Element of L; :: thesis: ( a <= b \ a implies a = Bottom L )
assume A1: a <= b \ a ; :: thesis: a = Bottom L
(b "/\" ('not' a)) "/\" a = b "/\" (('not' a) "/\" a) by LATTICE3:16
.= b "/\" (Bottom L) by Th34
.= Bottom L by WAYBEL_1:3 ;
hence a = Bottom L by A1, Th10; :: thesis: verum