let T be complete Lawson TopLattice; :: thesis: for X being finite Subset of T holds
( (uparrow X) ` is open & (downarrow X) ` is open )
let X be finite Subset of T; :: thesis: ( (uparrow X) ` is open & (downarrow X) ` is open )
deffunc H₁( Element of T) -> Element of K32( the carrier of T) = uparrow $1;
{ (uparrow x) where x is Element of T : x in X } c= bool the carrier of T

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (uparrow x) where x is Element of T : x in X } or z in bool the carrier of T )
assume z in { (uparrow x) where x is Element of T : x in X } ; :: thesis: z in bool the carrier of T
then ex x being Element of T st
( z = uparrow x & x in X ) ;
hence z in bool the carrier of T ; :: thesis: verum

end;

then reconsider upx = { (uparrow x) where x is Element of T : x in X } as Subset-Family of T ;
{ (downarrow x) where x is Element of T : x in X } c= bool the carrier of T

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (downarrow x) where x is Element of T : x in X } or z in bool the carrier of T )
assume z in { (downarrow x) where x is Element of T : x in X } ; :: thesis: z in bool the carrier of T
then ex x being Element of T st
( z = downarrow x & x in X ) ;
hence z in bool the carrier of T ; :: thesis: verum

end;

then reconsider dox = { (downarrow x) where x is Element of T : x in X } as Subset-Family of T ;
reconsider dox = dox as Subset-Family of T ;
reconsider upx = upx as Subset-Family of T ;
A1: uparrow X = union upx by YELLOW_9:4;

now :: thesis: for P being Subset of T st P in upx holds
P is closed

let P be Subset of T; :: thesis: ( P in upx implies P is closed )
assume P in upx ; :: thesis: P is closed
then ex x being Element of T st
( P = uparrow x & x in X ) ;
hence P is closed by WAYBEL19:38; :: thesis: verum

end;

then A2: upx is closed by TOPS_2:def 2;
A3: X is finite ;
{ H₁(x) where x is Element of T : x in X } is finite from FRAENKEL:sch 21(A3);
then uparrow X is closed by A2, A1, TOPS_2:21;
hence (uparrow X) ` is open by TOPS_1:3; :: thesis: (downarrow X) ` is open
deffunc H₂( Element of T) -> Element of K32( the carrier of T) = downarrow $1;
A4: downarrow X = union dox by YELLOW_9:4;

now :: thesis: for P being Subset of T st P in dox holds
P is closed

let P be Subset of T; :: thesis: ( P in dox implies P is closed )
assume P in dox ; :: thesis: P is closed
then ex x being Element of T st
( P = downarrow x & x in X ) ;
hence P is closed by WAYBEL19:38; :: thesis: verum

end;

then A5: dox is closed by TOPS_2:def 2;
{ H₂(x) where x is Element of T : x in X } is finite from FRAENKEL:sch 21(A3);
then downarrow X is closed by A5, A4, TOPS_2:21;
hence (downarrow X) ` is open by TOPS_1:3; :: thesis: verum