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 )
{ (uparrow x) where x is Element of T : x in X } c= bool the carrier of T

proof

let z be set ; :: 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 consider x being Element of T such that
A1: z = uparrow x and
x in X ;
thus z in bool the carrier of T by A1; :: thesis: verum

end;

then reconsider upx = { (uparrow x) where x is Element of T : x in X } as Subset-Family of T ;
reconsider upx = upx 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 set ; :: 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 consider x being Element of T such that
A2: z = downarrow x and
x in X ;
thus z in bool the carrier of T by A2; :: 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 ;

now

let P be Subset of T; :: thesis: ( P in upx implies P is closed )
assume P in upx ; :: thesis: P is closed
then consider x being Element of T such that
A3: P = uparrow x and
x in X ;
thus P is closed by A3, WAYBEL19:38; :: thesis: verum

end;

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

now

let P be Subset of T; :: thesis: ( P in dox implies P is closed )
assume P in dox ; :: thesis: P is closed
then consider x being Element of T such that
A7: P = downarrow x and
x in X ;
thus P is closed by A7, WAYBEL19:38; :: thesis: verum

end;

then A8: dox is closed by TOPS_2:def 2;
deffunc H₂( Element of T) -> Element of bool the carrier of T = downarrow $1;
A9: { H₂(x) where x is Element of T : x in X } is finite from FRAENKEL:sch 21(A5);
downarrow X = union dox by YELLOW_9:4;
then downarrow X is closed by A8, A9, TOPS_2:28;
hence (downarrow X) ` is open by TOPS_1:29; :: thesis: verum