let L be non empty antisymmetric upper-bounded RelStr ; :: thesis: for x being Element of L holds x <= Top L
let x be Element of L; :: thesis: x <= Top L
( {} is_>=_than x & ex_inf_of {} ,L ) by Th43;
hence x <= Top L by Th31; :: thesis: verum