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:2; :: thesis: verum
end;
assume A1: L is with_suprema ; :: thesis: ( not L is reflexive or not L is transitive or (Bottom L) "\/" x = x )
then A2: x <= (Bottom L) "\/" x by YELLOW_0:22;
assume ( L is reflexive & L is transitive ) ; :: thesis: (Bottom L) "\/" x = x
then A3: x <= x ;
Bottom L <= x by YELLOW_0:44;
then (Bottom L) "\/" x <= x by A1, A3, YELLOW_0:22;
hence (Bottom L) "\/" x = x by A2, ORDERS_2:2; :: thesis: verum