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