let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: for a being Element of L st a <= Bottom L holds
a = Bottom L
let a be Element of L; :: thesis: ( a <= Bottom L implies a = Bottom L )
A1: Bottom L <= a by YELLOW_0:44;
assume a <= Bottom L ; :: thesis: a = Bottom L
hence a = Bottom L by A1, YELLOW_0:def 3; :: thesis: verum