let L be antisymmetric with_suprema lower-bounded RelStr ; :: thesis: for a, b being Element of L st a "\/" b = Bottom L holds
( a = Bottom L & b = Bottom L )
let a, b be Element of L; :: thesis: ( a "\/" b = Bottom L implies ( a = Bottom L & b = Bottom L ) )
assume a "\/" b = Bottom L ; :: thesis: ( a = Bottom L & b = Bottom L )
then ( a <= Bottom L & b <= Bottom L ) by YELLOW_0:22;
hence ( a = Bottom L & b = Bottom L ) by Th19; :: thesis: verum