let L be antisymmetric upper-bounded with_suprema RelStr ; :: thesis: for X being Subset of L holds X "\/" {(Top L)} c= {(Top L)}
let X be Subset of L; :: thesis: X "\/" {(Top L)} c= {(Top L)}
A1: {(Top L)} "\/" X = { ((Top L) "\/" y) where y is Element of L : y in X } by YELLOW_4:15;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in X "\/" {(Top L)} or q in {(Top L)} )
assume q in X "\/" {(Top L)} ; :: thesis: q in {(Top L)}
then consider y being Element of L such that
A2: q = (Top L) "\/" y and
y in X by A1;
y "\/" (Top L) = Top L by WAYBEL_1:4;
hence q in {(Top L)} by A2, TARSKI:def 1; :: thesis: verum