let L be transitive antisymmetric with_infima lower-bounded RelStr ; :: thesis: for a being Element of holds a misses Bottom L
let a be Element of ; :: thesis: a misses Bottom L
a "/\" (Bottom L) = Bottom L by Th28;
hence a misses Bottom L by Def3; :: thesis: verum