let L be non empty upper-bounded Poset; :: thesis: not Top L in Irr L
assume Top L in Irr L ; :: thesis: contradiction
then Top L is completely-irreducible by Def4;
then "/\" ((uparrow (Top L)) \ {(Top L)}),L <> Top L by Th19;
then "/\" ({(Top L)} \ {(Top L)}),L <> Top L by WAYBEL_4:24;
then "/\" {} ,L <> Top L by XBOOLE_1:37;
hence contradiction by YELLOW_0:def 12; :: thesis: verum