let L be lower-bounded sup-Semilattice; :: thesis: for I being Ideal of L holds {(Bottom L)} c= I
let I be Ideal of L; :: thesis: {(Bottom L)} c= I
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {(Bottom L)} or a in I )
assume a in {(Bottom L)} ; :: thesis: a in I
then a = Bottom L by TARSKI:def 1;
hence a in I by Th21; :: thesis: verum