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

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