let L be non empty reflexive RelStr ; :: thesis: for A being Subset of L st A in sigma L holds
A in xi L
let A be Subset of L; :: thesis: ( A in sigma L implies A in xi L )
A1: the topology of (ConvergenceSpace (Scott-Convergence L)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L)) by Th22, Th23;
assume A in sigma L ; :: thesis: A in xi L
hence A in xi L by A1; :: thesis: verum