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

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