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 ) by STRUCT_0:def 10; :: 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 & y >= Bottom L & y <= Bottom L ) by A1, YELLOW_0:44, YELLOW_0:45;
then ( x = Bottom L & y = Bottom L ) by ORDERS_2:25;
hence x = y ; :: thesis: verum