let L be non empty antisymmetric bounded RelStr ; :: thesis: ( L is trivial iff Top L = Bottom L )
thus ( L is trivial implies Top L = Bottom L ) ; :: thesis: ( Top L = Bottom L implies L is trivial )
assume A1: Top L = Bottom L ; :: thesis: L is trivial
let x, y be Element of L; :: according to STRUCT_0:def 10 :: thesis: x = y
reconsider x = x, y = y as Element of L ;
( x >= Bottom L & x <= Bottom L ) by A1, YELLOW_0:44, YELLOW_0:45;
then A2: x = Bottom L by ORDERS_2:2;
( y >= Bottom L & y <= Bottom L ) by A1, YELLOW_0:44, YELLOW_0:45;
hence x = y by A2, ORDERS_2:2; :: thesis: verum