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: sigma L = the topology of L by Th23;
A3: the carrier of (InclPoset the topology of L) = the topology of L by YELLOW_1:1;
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 } ;
V in sigma L by A2, A3;
then A5: V = union { (wayabove x) where x is Element of L : x in V } by A1, Th33;
set wV = waybelow V;

now

let x be set ; :: 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
A6: ( x in xU & xU in { (wayabove x) where x is Element of L : x in V } ) by A5, TARSKI:def 4;
consider y being Element of L such that
A7: ( xU = wayabove y & 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 A3, A7, PRE_TOPC:def 5;
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
A8: ( y in DD & DD in D ) by A7, TARSKI:def 4;
DD in sigma L by A2, A3, A8;
then reconsider DD = DD as Subset of L ;
DD is open by A3, A8, PRE_TOPC:def 5;
then DD is upper by WAYBEL11:def 4;
then A9: uparrow y c= DD by A8, WAYBEL11:42;
wayabove y c= uparrow y by WAYBEL_3:11;
then A10: wayabove y c= DD by A9, XBOOLE_1:1;
reconsider d = DD as Element of (InclPoset the topology of L) by A8;
take d ; :: thesis: ( d in D & xU <= d )
thus d in D by A8; :: thesis: xU <= d
thus xU <= d by A7, A10, YELLOW_1:3; :: thesis: verum

end;

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

end;

assume x in union (waybelow V) ; :: thesis: x in V
then consider X being set such that
A11: ( x in X & X in waybelow V ) by TARSKI:def 4;
reconsider X = X as Element of (InclPoset the topology of L) by A11;
X << V by A11, WAYBEL_3:7;
then X <= V by WAYBEL_3:1;
then X c= V by YELLOW_1:3;
hence x in V by A11; :: 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