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

proof

assume A1: ( L is with_infima & L is transitive & L is reflexive ) ; :: thesis: (Top L) "/\" x = x
then x "/\" x <= (Top L) "/\" x by Th1, YELLOW_0:45;
then A2: x <= (Top L) "/\" x by A1, YELLOW_0:25;
(Top L) "/\" x <= x by A1, YELLOW_0:23;
hence (Top L) "/\" x = x by A2, ORDERS_2:2; :: thesis: verum

end;

assume L is with_suprema ; :: thesis: (Top L) "\/" x = Top L
then ( (Top L) "\/" x <= Top L & Top L <= (Top L) "\/" x ) by YELLOW_0:22, YELLOW_0:45;
hence (Top L) "\/" x = Top L by ORDERS_2:2; :: thesis: verum