let L be non empty antisymmetric upper-bounded with_infima RelStr ; :: thesis: Top L is irreducible
let x, y be Element of L; :: according to WAYBEL_6:def 2 :: thesis: ( not Top L = x "/\" y or x = Top L or y = Top L )
assume x "/\" y = Top L ; :: thesis: ( x = Top L or y = Top L )
then A1: ( x >= Top L & y >= Top L ) by YELLOW_0:23;
( x <= Top L or y <= Top L ) by YELLOW_0:45;
hence ( x = Top L or y = Top L ) by A1, ORDERS_2:2; :: thesis: verum