let L be non empty antisymmetric upper-bounded RelStr ; :: thesis: for X being non empty upper Subset of L holds Top L in X
let X be non empty upper Subset of L; :: thesis: Top L in X
consider y being object such that
A1: y in X by XBOOLE_0:def 1;
reconsider y = y as Element of X by A1;
Top L >= y by YELLOW_0:45;
hence Top L in X by WAYBEL_0:def 20; :: thesis: verum