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