let L be complete Scott TopLattice; :: thesis:
assume A1: L is continuous ; :: thesis:
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:
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:

let x be object ; :: thesis:

hereby :: thesis:

assume x in V ; :: thesis:
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:
assume V <= sup D ; :: thesis:
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:
thus d in D by A10; :: thesis:
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:

end;

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

end;

assume x in union (waybelow V) ; :: thesis:
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:

end;

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

end;

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