reconsider y = x as Element of (Omega T) ;
Cl {y} = downarrow y by Th22;
hence ( not Cl {x} is empty & Cl {x} is lower & Cl {x} is directed ) ; :: thesis: verum