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 )
assume A1: A in sigma L ; :: thesis: A in xi L
the topology of (ConvergenceSpace (Scott-Convergence L)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L)) by Th21, Th22;
hence A in xi L by A1; :: thesis: verum