let L be antisymmetric upper-bounded with_suprema RelStr ; :: thesis: for X being non empty Subset of L holds X "\/" {(Top L)} = {(Top L)}

let X be non empty Subset of L; :: thesis: X "\/" {(Top L)} = {(Top L)}

thus X "\/" {(Top L)} c= {(Top L)} by Th12; :: according to XBOOLE_0:def 10 :: thesis: {(Top L)} c= X "\/" {(Top L)}

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {(Top L)} or q in X "\/" {(Top L)} )

assume q in {(Top L)} ; :: thesis: q in X "\/" {(Top L)}

then A1: ( X "\/" {(Top L)} = { ((Top L) "\/" y) where y is Element of L : y in X } & q = Top L ) by TARSKI:def 1, YELLOW_4:15;

consider y being object such that

A2: y in X by XBOOLE_0:def 1;

reconsider y = y as Element of X by A2;

(Top L) "\/" y = Top L by WAYBEL_1:4;

hence q in X "\/" {(Top L)} by A1; :: thesis: verum

let X be non empty Subset of L; :: thesis: X "\/" {(Top L)} = {(Top L)}

thus X "\/" {(Top L)} c= {(Top L)} by Th12; :: according to XBOOLE_0:def 10 :: thesis: {(Top L)} c= X "\/" {(Top L)}

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {(Top L)} or q in X "\/" {(Top L)} )

assume q in {(Top L)} ; :: thesis: q in X "\/" {(Top L)}

then A1: ( X "\/" {(Top L)} = { ((Top L) "\/" y) where y is Element of L : y in X } & q = Top L ) by TARSKI:def 1, YELLOW_4:15;

consider y being object such that

A2: y in X by XBOOLE_0:def 1;

reconsider y = y as Element of X by A2;

(Top L) "\/" y = Top L by WAYBEL_1:4;

hence q in X "\/" {(Top L)} by A1; :: thesis: verum