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