let L be non empty Boolean RelStr ; :: thesis: for a being Element of L holds a \ (Bottom L) = a
let a be Element of L; :: thesis: a \ (Bottom L) = a
thus a \ (Bottom L) = a "/\" (Top L) by Th65
.= a by WAYBEL_1:5 ; :: thesis: verum