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

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