let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; :: thesis: for x being Element of T holds downarrow x is closed
let x be Element of T; :: thesis: downarrow x is closed
( downarrow x is closed_under_directed_sups & downarrow x is lower ) by Th8;
hence downarrow x is closed by Th7; :: thesis: verum