let L be complete Scott TopLattice; :: thesis: ( L is continuous implies InclPoset (sigma L) is continuous )
assume A1: L is continuous ; :: thesis: InclPoset (sigma L) is continuous
set IPs = InclPoset the topology of L;
A2: the carrier of (InclPoset the topology of L) = the topology of L by YELLOW_1:1;
A3: sigma L = the topology of L by Th23;
InclPoset the topology of L is satisfying_axiom_of_approximation

proof

let V be Element of (InclPoset the topology of L); :: according to WAYBEL_3:def 5 :: thesis: V = "\/" ((waybelow V),(InclPoset the topology of L))
set VV = { (wayabove x) where x is Element of L : x in V } ;
set wV = waybelow V;
V in sigma L by A3, A2;
then A4: V = union { (wayabove x) where x is Element of L : x in V } by A1, Th33;

now :: thesis: for x being object holds
( ( x in V implies x in union (waybelow V) ) & ( x in union (waybelow V) implies x in V ) )

let x be object ; :: thesis: ( ( x in V implies x in union (waybelow V) ) & ( x in union (waybelow V) implies x in V ) )

hereby :: thesis: ( x in union (waybelow V) implies x in V )

assume x in V ; :: thesis: x in union (waybelow V)
then consider xU being set such that
A5: x in xU and
A6: xU in { (wayabove x) where x is Element of L : x in V } by A4, TARSKI:def 4;
consider y being Element of L such that
A7: xU = wayabove y and
A8: y in V by A6;
wayabove y is open by A1, WAYBEL11:36;
then reconsider xU = xU as Element of (InclPoset the topology of L) by A2, A7, PRE_TOPC:def 2;
xU << V

proof

let D be non empty directed Subset of (InclPoset the topology of L); :: according to WAYBEL_3:def 1 :: thesis: ( not V <= "\/" (D,(InclPoset the topology of L)) or ex b₁ being Element of the carrier of (InclPoset the topology of L) st
( b₁ in D & xU <= b₁ ) )
assume V <= sup D ; :: thesis: ex b₁ being Element of the carrier of (InclPoset the topology of L) st
( b₁ in D & xU <= b₁ )
then V c= sup D by YELLOW_1:3;
then V c= union D by YELLOW_1:22;
then consider DD being set such that
A9: y in DD and
A10: DD in D by A8, TARSKI:def 4;
DD in sigma L by A3, A2, A10;
then reconsider DD = DD as Subset of L ;
DD is open by A2, A10, PRE_TOPC:def 2;
then DD is upper by WAYBEL11:def 4;
then A11: uparrow y c= DD by A9, WAYBEL11:42;
reconsider d = DD as Element of (InclPoset the topology of L) by A10;
take d ; :: thesis: ( d in D & xU <= d )
thus d in D by A10; :: thesis: xU <= d
wayabove y c= uparrow y by WAYBEL_3:11;
then wayabove y c= DD by A11;
hence xU <= d by A7, YELLOW_1:3; :: thesis: verum

end;

then xU in waybelow V ;
hence x in union (waybelow V) by A5, TARSKI:def 4; :: thesis: verum

end;

assume x in union (waybelow V) ; :: thesis: x in V
then consider X being set such that
A12: x in X and
A13: X in waybelow V by TARSKI:def 4;
reconsider X = X as Element of (InclPoset the topology of L) by A13;
X << V by A13, WAYBEL_3:7;
then X <= V by WAYBEL_3:1;
then X c= V by YELLOW_1:3;
hence x in V by A12; :: thesis: verum

end;

then V = union (waybelow V) by TARSKI:2;
hence V = "\/" ((waybelow V),(InclPoset the topology of L)) by YELLOW_1:22; :: thesis: verum

end;

hence InclPoset (sigma L) is continuous by Th23; :: thesis: verum