let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: for x being Element of L holds
( ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) & ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x ) )
let x be Element of L; :: thesis: ( ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) & ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x ) )
thus ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) :: thesis: ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x )

proof

assume L is with_infima ; :: thesis: (Bottom L) "/\" x = Bottom L
then ( Bottom L <= (Bottom L) "/\" x & (Bottom L) "/\" x <= Bottom L ) by YELLOW_0:23, YELLOW_0:44;
hence (Bottom L) "/\" x = Bottom L by ORDERS_2:25; :: thesis: verum

end;

assume A1: L is with_suprema ; :: thesis: ( not L is reflexive or not L is transitive or (Bottom L) "\/" x = x )
assume ( L is reflexive & L is transitive ) ; :: thesis: (Bottom L) "\/" x = x
then A2: x <= x by ORDERS_2:24;
Bottom L <= x by YELLOW_0:44;
then ( x <= (Bottom L) "\/" x & (Bottom L) "\/" x <= x ) by A1, A2, YELLOW_0:22;
hence (Bottom L) "\/" x = x by ORDERS_2:25; :: thesis: verum