:: YELLOW15 semantic presentation

begin

scheme :: YELLOW15:sch 1
SeqLambda1C{ F1() ->  Nat, F2() ->  non empty set , P1[ set ], F3( set ) ->  set , F4( set ) ->  set } :
 ex p being FinSequence of F2() st
( len p = F1() & ( for i being Nat st i in Seg F1() holds
( ( P1[i] implies p . i = F3(i) ) & ( P1[i] implies p . i = F4(i) ) ) ) )
provided
A1: for i being Nat st i in Seg F1() holds
( ( P1[i] implies F3(i) in F2() ) & ( P1[i] implies F4(i) in F2() ) )
proof
A2: for x being set st x in Seg F1() holds
( ( P1[x] implies F3(x) in F2() ) & ( P1[x] implies F4(x) in F2() ) ) by A1;
consider p being Function of (Seg F1()),F2() such that
A3: for x being set st x in Seg F1() holds
( ( P1[x] implies p . x = F3(x) ) & ( P1[x] implies p . x = F4(x) ) ) from FUNCT_2:sch_5(A2);
A4: dom p = Seg F1() by FUNCT_2:def_1;
then reconsider p = p as FinSequence by FINSEQ_1:def_2;
 rng p c= F2() by RELAT_1:def_19;
then reconsider p = p as FinSequence of F2() by FINSEQ_1:def_4;
take  p ; ::_thesis: ( len p = F1() & ( for i being Nat st i in Seg F1() holds
( ( P1[i] implies p . i = F3(i) ) & ( P1[i] implies p . i = F4(i) ) ) ) )
 F1() is Element of NAT by ORDINAL1:def_12;
hence  ( len p = F1() & ( for i being Nat st i in Seg F1() holds
( ( P1[i] implies p . i = F3(i) ) & ( P1[i] implies p . i = F4(i) ) ) ) ) by A3, A4, FINSEQ_1:def_3; ::_thesis: verum
end;

begin

definition
let X be set ;
let p be FinSequence of bool X;
let q be FinSequence of BOOLEAN ;
func MergeSequence (p,q) ->  FinSequence of bool X means :Def1: :: YELLOW15:def 1
( len it = len p & ( for i being Nat st i in dom p holds
it . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) );
existence
 ex b1 being FinSequence of bool X st
( len b1 = len p & ( for i being Nat st i in dom p holds
b1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) )
proof
deffunc H1( Nat) ->  set = IFEQ ((q . $1),TRUE,(p . $1),(X \ (p . $1)));
consider r being FinSequence such that
A1: len r = len p and
A2: for i being Nat st i in dom r holds
r . i = H1(i) from FINSEQ_1:sch_2();
 rng r c= bool X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng r or z in bool X )
assume  z in rng r ; ::_thesis: z in bool X
then consider i being Nat such that
A3: i in dom r and
A4: r . i = z by FINSEQ_2:10;
A5: z = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) by A2, A3, A4;
 i in Seg (len p) by A1, A3, FINSEQ_1:def_3;
then A6: i in dom p by FINSEQ_1:def_3;
now__::_thesis:_z_in_bool_X
percases ( q . i = TRUE or q . i <> TRUE ) ;
suppose q . i = TRUE ; ::_thesis: z in bool X
then  z = p . i by A5, FUNCOP_1:def_8;
hence  z in bool X by A6, FINSEQ_2:11; ::_thesis: verum
end;
suppose q . i <> TRUE ; ::_thesis: z in bool X
then  z = X \ (p . i) by A5, FUNCOP_1:def_8;
hence  z in bool X ; ::_thesis: verum
end;
end;
end;
hence  z in bool X ; ::_thesis: verum
end;
then reconsider r = r as FinSequence of bool X by FINSEQ_1:def_4;
take  r ; ::_thesis: ( len r = len p & ( for i being Nat st i in dom p holds
r . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) )
 dom p = dom r by A1, FINSEQ_3:29;
hence  ( len r = len p & ( for i being Nat st i in dom p holds
r . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of bool X st len b1 = len p & ( for i being Nat st i in dom p holds
b1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) & len b2 = len p & ( for i being Nat st i in dom p holds
b2 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) holds
b1 = b2
proof
let r1, r2 be FinSequence of bool X; ::_thesis: ( len r1 = len p & ( for i being Nat st i in dom p holds
r1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) & len r2 = len p & ( for i being Nat st i in dom p holds
r2 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) implies r1 = r2 )
assume that
A7: len r1 = len p and
A8: for i being Nat st i in dom p holds
r1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) and
A9: len r2 = len p and
A10: for i being Nat st i in dom p holds
r2 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ; ::_thesis: r1 = r2
A11: dom r1 = Seg (len p) by A7, FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_r1_holds_
r1_._i_=_r2_._i
let i be Nat; ::_thesis: ( i in dom r1 implies r1 . i = r2 . i )
assume  i in dom r1 ; ::_thesis: r1 . i = r2 . i
then A12: i in dom p by A11, FINSEQ_1:def_3;
hence r1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) by A8
.= r2 . i by A10, A12 ;
::_thesis: verum
end;
hence  r1 = r2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines MergeSequence YELLOW15:def_1_:_
 for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for b4 being FinSequence of bool X holds
( b4 = MergeSequence (p,q) iff ( len b4 = len p & ( for i being Nat st i in dom p holds
b4 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) ) );

theorem :: YELLOW15:1
canceled;

theorem :: YELLOW15:2
canceled;

theorem :: YELLOW15:3
canceled;

theorem Th4: :: YELLOW15:4
for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p
proof
let X be set ; ::_thesis: for p being FinSequence of bool X
for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p
let p be FinSequence of bool X; ::_thesis: for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p
let q be FinSequence of BOOLEAN ; ::_thesis: dom (MergeSequence (p,q)) = dom p
thus  dom (MergeSequence (p,q)) = Seg (len (MergeSequence (p,q))) by FINSEQ_1:def_3
.= Seg (len p) by Def1
.= dom p by FINSEQ_1:def_3 ; ::_thesis: verum
end;

theorem Th5: :: YELLOW15:5
for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for i being Nat st q . i = TRUE holds
(MergeSequence (p,q)) . i = p . i
proof
let X be set ; ::_thesis: for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for i being Nat st q . i = TRUE holds
(MergeSequence (p,q)) . i = p . i
let p be FinSequence of bool X; ::_thesis: for q being FinSequence of BOOLEAN
for i being Nat st q . i = TRUE holds
(MergeSequence (p,q)) . i = p . i
let q be FinSequence of BOOLEAN ; ::_thesis: for i being Nat st q . i = TRUE holds
(MergeSequence (p,q)) . i = p . i
let i be Nat; ::_thesis: ( q . i = TRUE implies (MergeSequence (p,q)) . i = p . i )
assume A1: q . i = TRUE ; ::_thesis: (MergeSequence (p,q)) . i = p . i
now__::_thesis:_(MergeSequence_(p,q))_._i_=_p_._i
percases ( i in dom p or not i in dom p ) ;
suppose i in dom p ; ::_thesis: (MergeSequence (p,q)) . i = p . i
hence (MergeSequence (p,q)) . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) by Def1
.= p . i by A1, FUNCOP_1:def_8 ;
::_thesis: verum
end;
supposeA2: not i in dom p ; ::_thesis: (MergeSequence (p,q)) . i = p . i
dom p = Seg (len p) by FINSEQ_1:def_3
.= Seg (len (MergeSequence (p,q))) by Def1
.= dom (MergeSequence (p,q)) by FINSEQ_1:def_3 ;
hence (MergeSequence (p,q)) . i = {} by A2, FUNCT_1:def_2
.= p . i by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;
hence  (MergeSequence (p,q)) . i = p . i ; ::_thesis: verum
end;

theorem Th6: :: YELLOW15:6
for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for i being Nat st i in dom p & q . i = FALSE holds
(MergeSequence (p,q)) . i = X \ (p . i)
proof
let X be set ; ::_thesis: for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for i being Nat st i in dom p & q . i = FALSE holds
(MergeSequence (p,q)) . i = X \ (p . i)
let p be FinSequence of bool X; ::_thesis: for q being FinSequence of BOOLEAN
for i being Nat st i in dom p & q . i = FALSE holds
(MergeSequence (p,q)) . i = X \ (p . i)
let q be FinSequence of BOOLEAN ; ::_thesis: for i being Nat st i in dom p & q . i = FALSE holds
(MergeSequence (p,q)) . i = X \ (p . i)
let i be Nat; ::_thesis: ( i in dom p & q . i = FALSE implies (MergeSequence (p,q)) . i = X \ (p . i) )
assume that
A1: i in dom p and
A2: q . i = FALSE ; ::_thesis: (MergeSequence (p,q)) . i = X \ (p . i)
thus (MergeSequence (p,q)) . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) by A1, Def1
.= X \ (p . i) by A2, FUNCOP_1:def_8 ; ::_thesis: verum
end;

theorem :: YELLOW15:7
for X being set
for q being FinSequence of BOOLEAN holds len (MergeSequence ((<*> (bool X)),q)) = 0
proof
let X be set ; ::_thesis: for q being FinSequence of BOOLEAN holds len (MergeSequence ((<*> (bool X)),q)) = 0
let q be FinSequence of BOOLEAN ; ::_thesis: len (MergeSequence ((<*> (bool X)),q)) = 0
thus  len (MergeSequence ((<*> (bool X)),q)) = len (<*> (bool X)) by Def1
.= 0 ; ::_thesis: verum
end;

theorem Th8: :: YELLOW15:8
for X being set
for q being FinSequence of BOOLEAN holds MergeSequence ((<*> (bool X)),q) = <*> (bool X)
proof
let X be set ; ::_thesis: for q being FinSequence of BOOLEAN holds MergeSequence ((<*> (bool X)),q) = <*> (bool X)
let q be FinSequence of BOOLEAN ; ::_thesis: MergeSequence ((<*> (bool X)),q) = <*> (bool X)
len (MergeSequence ((<*> (bool X)),q)) = len (<*> (bool X)) by Def1
.= 0 ;
hence  MergeSequence ((<*> (bool X)),q) = <*> (bool X) ; ::_thesis: verum
end;

theorem :: YELLOW15:9
for X being set
for x being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x*>,q)) = 1
proof
let X be set ; ::_thesis: for x being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x*>,q)) = 1
let x be Subset of X; ::_thesis: for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x*>,q)) = 1
let q be FinSequence of BOOLEAN ; ::_thesis: len (MergeSequence (<*x*>,q)) = 1
thus  len (MergeSequence (<*x*>,q)) = len <*x*> by Def1
.= 1 by FINSEQ_1:39 ; ::_thesis: verum
end;

theorem :: YELLOW15:10
for X being set
for x being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x ) )
proof
let X be set ; ::_thesis: for x being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x ) )
let x be Subset of X; ::_thesis: for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x ) )
let q be FinSequence of BOOLEAN ; ::_thesis: ( ( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x ) )
thus  ( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x ) ::_thesis: ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x )
proof
assume  q . 1 = TRUE ; ::_thesis: (MergeSequence (<*x*>,q)) . 1 = x
hence (MergeSequence (<*x*>,q)) . 1 = <*x*> . 1 by Th5
.= x by FINSEQ_1:40 ;
::_thesis: verum
end;
 1 in Seg 1 by FINSEQ_1:1;
then A1: 1 in dom <*x*> by FINSEQ_1:38;
assume  q . 1 = FALSE ; ::_thesis: (MergeSequence (<*x*>,q)) . 1 = X \ x
hence (MergeSequence (<*x*>,q)) . 1 = X \ (<*x*> . 1) by A1, Th6
.= X \ x by FINSEQ_1:40 ;
::_thesis: verum
end;

theorem :: YELLOW15:11
for X being set
for x, y being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2
proof
let X be set ; ::_thesis: for x, y being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2
let x, y be Subset of X; ::_thesis: for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2
let q be FinSequence of BOOLEAN ; ::_thesis: len (MergeSequence (<*x,y*>,q)) = 2
thus  len (MergeSequence (<*x,y*>,q)) = len <*x,y*> by Def1
.= 2 by FINSEQ_1:44 ; ::_thesis: verum
end;

theorem :: YELLOW15:12
for X being set
for x, y being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )
proof
let X be set ; ::_thesis: for x, y being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )
let x, y be Subset of X; ::_thesis: for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )
let q be FinSequence of BOOLEAN ; ::_thesis: ( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )
thus  ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) ::_thesis: ( ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )
proof
assume  q . 1 = TRUE ; ::_thesis: (MergeSequence (<*x,y*>,q)) . 1 = x
hence (MergeSequence (<*x,y*>,q)) . 1 = <*x,y*> . 1 by Th5
.= x by FINSEQ_1:44 ;
::_thesis: verum
end;
 2 in Seg 2 by FINSEQ_1:1;
then A1: 2 in dom <*x,y*> by FINSEQ_1:89;
 1 in Seg 2 by FINSEQ_1:1;
then A2: 1 in dom <*x,y*> by FINSEQ_1:89;
thus  ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) ::_thesis: ( ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )
proof
assume  q . 1 = FALSE ; ::_thesis: (MergeSequence (<*x,y*>,q)) . 1 = X \ x
hence (MergeSequence (<*x,y*>,q)) . 1 = X \ (<*x,y*> . 1) by A2, Th6
.= X \ x by FINSEQ_1:44 ;
::_thesis: verum
end;
thus  ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) ::_thesis: ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y )
proof
assume  q . 2 = TRUE ; ::_thesis: (MergeSequence (<*x,y*>,q)) . 2 = y
hence (MergeSequence (<*x,y*>,q)) . 2 = <*x,y*> . 2 by Th5
.= y by FINSEQ_1:44 ;
::_thesis: verum
end;
assume  q . 2 = FALSE ; ::_thesis: (MergeSequence (<*x,y*>,q)) . 2 = X \ y
hence (MergeSequence (<*x,y*>,q)) . 2 = X \ (<*x,y*> . 2) by A1, Th6
.= X \ y by FINSEQ_1:44 ;
::_thesis: verum
end;

theorem :: YELLOW15:13
for X being set
for x, y, z being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y,z*>,q)) = 3
proof
let X be set ; ::_thesis: for x, y, z being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y,z*>,q)) = 3
let x, y, z be Subset of X; ::_thesis: for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y,z*>,q)) = 3
let q be FinSequence of BOOLEAN ; ::_thesis: len (MergeSequence (<*x,y,z*>,q)) = 3
thus  len (MergeSequence (<*x,y,z*>,q)) = len <*x,y,z*> by Def1
.= 3 by FINSEQ_1:45 ; ::_thesis: verum
end;

theorem :: YELLOW15:14
for X being set
for x, y, z being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 2 = X \ y ) & ( q . 3 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 3 = z ) & ( q . 3 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z ) )
proof
let X be set ; ::_thesis: for x, y, z being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 2 = X \ y ) & ( q . 3 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 3 = z ) & ( q . 3 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z ) )
let x, y, z be Subset of X; ::_thesis: for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 2 = X \ y ) & ( q . 3 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 3 = z ) & ( q . 3 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z ) )
let q be FinSequence of BOOLEAN ; ::_thesis: ( ( q . 1 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 2 = X \ y ) & ( q . 3 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 3 = z ) & ( q . 3 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z ) )
thus  ( q . 1 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 1 = x ) ::_thesis: ( ( q . 1 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 2 = X \ y ) & ( q . 3 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 3 = z ) & ( q . 3 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z ) )
proof
assume  q . 1 = TRUE ; ::_thesis: (MergeSequence (<*x,y,z*>,q)) . 1 = x
hence (MergeSequence (<*x,y,z*>,q)) . 1 = <*x,y,z*> . 1 by Th5
.= x by FINSEQ_1:45 ;
::_thesis: verum
end;
 3 in Seg 3 by FINSEQ_1:1;
then A1: 3 in dom <*x,y,z*> by FINSEQ_1:89;
 1 in Seg 3 by FINSEQ_1:1;
then A2: 1 in dom <*x,y,z*> by FINSEQ_1:89;
thus  ( q . 1 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 1 = X \ x ) ::_thesis: ( ( q . 2 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 2 = X \ y ) & ( q . 3 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 3 = z ) & ( q . 3 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z ) )
proof
assume  q . 1 = FALSE ; ::_thesis: (MergeSequence (<*x,y,z*>,q)) . 1 = X \ x
hence (MergeSequence (<*x,y,z*>,q)) . 1 = X \ (<*x,y,z*> . 1) by A2, Th6
.= X \ x by FINSEQ_1:45 ;
::_thesis: verum
end;
thus  ( q . 2 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 2 = y ) ::_thesis: ( ( q . 2 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 2 = X \ y ) & ( q . 3 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 3 = z ) & ( q . 3 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z ) )
proof
assume  q . 2 = TRUE ; ::_thesis: (MergeSequence (<*x,y,z*>,q)) . 2 = y
hence (MergeSequence (<*x,y,z*>,q)) . 2 = <*x,y,z*> . 2 by Th5
.= y by FINSEQ_1:45 ;
::_thesis: verum
end;
 2 in Seg 3 by FINSEQ_1:1;
then A3: 2 in dom <*x,y,z*> by FINSEQ_1:89;
thus  ( q . 2 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 2 = X \ y ) ::_thesis: ( ( q . 3 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 3 = z ) & ( q . 3 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z ) )
proof
assume  q . 2 = FALSE ; ::_thesis: (MergeSequence (<*x,y,z*>,q)) . 2 = X \ y
hence (MergeSequence (<*x,y,z*>,q)) . 2 = X \ (<*x,y,z*> . 2) by A3, Th6
.= X \ y by FINSEQ_1:45 ;
::_thesis: verum
end;
thus  ( q . 3 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 3 = z ) ::_thesis: ( q . 3 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z )
proof
assume  q . 3 = TRUE ; ::_thesis: (MergeSequence (<*x,y,z*>,q)) . 3 = z
hence (MergeSequence (<*x,y,z*>,q)) . 3 = <*x,y,z*> . 3 by Th5
.= z by FINSEQ_1:45 ;
::_thesis: verum
end;
assume  q . 3 = FALSE ; ::_thesis: (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z
hence (MergeSequence (<*x,y,z*>,q)) . 3 = X \ (<*x,y,z*> . 3) by A1, Th6
.= X \ z by FINSEQ_1:45 ;
::_thesis: verum
end;

theorem Th15: :: YELLOW15:15
for X being set
for p being FinSequence of bool X holds  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  is Subset-Family of X
proof
let X be set ; ::_thesis: for p being FinSequence of bool X holds  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  is Subset-Family of X
let p be FinSequence of bool X; ::_thesis:  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  is Subset-Family of X
  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  c= bool X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  or z in bool X )
assume  z in  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ; ::_thesis: z in bool X
then  ex q being FinSequence of BOOLEAN st
( z = Intersect (rng (MergeSequence (p,q))) & len q = len p ) ;
hence  z in bool X ; ::_thesis: verum
end;
hence   {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  is Subset-Family of X ; ::_thesis: verum
end;

registration
cluster  ->  boolean-valued for FinSequence of BOOLEAN ;
coherence
 for b1 being FinSequence of BOOLEAN holds b1 is boolean-valued
proof
let f be FinSequence of BOOLEAN ; ::_thesis: f is boolean-valued
thus  rng f c= BOOLEAN ; :: according to MARGREL1:def_16 ::_thesis: verum
end;
end;

definition
let X be set ;
let Y be finite Subset-Family of X;
func Components Y ->  Subset-Family of X means :Def2: :: YELLOW15:def 2
 ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & it =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  );
existence
 ex b1 being Subset-Family of X ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & b1 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  )
proof
consider p being FinSequence such that
A1: rng p = Y and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of bool X by A1, FINSEQ_1:def_4;
reconsider C =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  as Subset-Family of X by Th15;
take  C ; ::_thesis: ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & C =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  )
take  p ; ::_thesis: ( len p = card Y & rng p = Y & C =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  )
thus  ( len p = card Y & rng p = Y & C =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) by A1, A2, FINSEQ_4:62; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of X st ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & b1 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) & ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & b2 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) holds
b1 = b2
proof
let C1, C2 be Subset-Family of X; ::_thesis: ( ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & C1 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) & ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & C2 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) implies C1 = C2 )
assume that
A3: ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & C1 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) and
A4: ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & C2 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) ; ::_thesis: C1 = C2
consider p1 being FinSequence of bool X such that
A5: len p1 = card Y and
A6: rng p1 = Y and
A7: C1 =  {  (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1  }  by A3;
consider p2 being FinSequence of bool X such that
A8: len p2 = card Y and
A9: rng p2 = Y and
A10: C2 =  {  (Intersect (rng (MergeSequence (p2,q)))) where q is FinSequence of BOOLEAN : len q = len p2  }  by A4;
A11: p2 is one-to-one by A8, A9, FINSEQ_4:62;
A12: p1 is one-to-one by A5, A6, FINSEQ_4:62;
now__::_thesis:_for_P_being_Subset_of_X_holds_
(_(_P_in_C1_implies_P_in_C2_)_&_(_P_in_C2_implies_P_in_C1_)_)
let P be Subset of X; ::_thesis: ( ( P in C1 implies P in C2 ) & ( P in C2 implies P in C1 ) )
thus  ( P in C1 implies P in C2 ) ::_thesis: ( P in C2 implies P in C1 )
proof
 p1 is Function of (dom p1),(rng p1) by FUNCT_2:1;
then A13: p1 " is Function of (rng p1),(dom p1) by A12, FUNCT_2:25;
 p2 is FinSequence of rng p1 by A6, A9, FINSEQ_1:def_4;
then A14: (p1 ") * p2 is FinSequence of dom p1 by A13, FINSEQ_2:32;
assume  P in C1 ; ::_thesis: P in C2
then consider q being FinSequence of BOOLEAN  such that
A15: P = Intersect (rng (MergeSequence (p1,q))) and
A16: len q = len p1 by A7;
A17: dom p1 = Seg (len q) by A16, FINSEQ_1:def_3
.= dom q by FINSEQ_1:def_3 ;
then  q is Function of (dom p1),BOOLEAN by FINSEQ_2:26;
then  q * ((p1 ") * p2) is FinSequence of BOOLEAN by A14, FINSEQ_2:32;
then reconsider q1 = (q * (p1 ")) * p2 as FinSequence of BOOLEAN by RELAT_1:36;
A18: rng p2 = dom (p1 ") by A6, A9, A12, FUNCT_1:33;
then A19: dom ((p1 ") * p2) = dom p2 by RELAT_1:27;
rng ((p1 ") * p2) = rng (p1 ") by A18, RELAT_1:28
.= dom q by A12, A17, FUNCT_1:33 ;
then A20: dom (q * ((p1 ") * p2)) = dom p2 by A19, RELAT_1:27;
A21: rng p1 = dom (p2 ") by A6, A9, A11, FUNCT_1:33;
then A22: dom ((p2 ") * p1) = dom p1 by RELAT_1:27;
A23: Seg (len q1) = dom q1 by FINSEQ_1:def_3
.= dom p2 by A20, RELAT_1:36
.= Seg (len p2) by FINSEQ_1:def_3 ;
then A24: dom p2 = Seg (len q1) by FINSEQ_1:def_3
.= dom q1 by FINSEQ_1:def_3 ;
rng ((p2 ") * p1) = rng (p2 ") by A21, RELAT_1:28
.= dom q1 by A11, A24, FUNCT_1:33 ;
then A25: dom (q1 * ((p2 ") * p1)) = dom p1 by A22, RELAT_1:27;
A26: (q1 * (p2 ")) * p1 = ((q * (p1 ")) * p2) * ((p2 ") * p1) by RELAT_1:36
.= (q * (p1 ")) * (p2 * ((p2 ") * p1)) by RELAT_1:36
.= (q * (p1 ")) * ((p2 * (p2 ")) * p1) by RELAT_1:36
.= (q * (p1 ")) * ((id (rng p2)) * p1) by A11, FUNCT_1:39
.= (q * (p1 ")) * p1 by A6, A9, RELAT_1:54
.= q * ((p1 ") * p1) by RELAT_1:36
.= q * (id (dom p1)) by A12, FUNCT_1:39
.= q by A17, RELAT_1:52 ;
A27: rng (MergeSequence (p1,q)) c= rng (MergeSequence (p2,q1))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (MergeSequence (p1,q)) or z in rng (MergeSequence (p2,q1)) )
assume  z in rng (MergeSequence (p1,q)) ; ::_thesis: z in rng (MergeSequence (p2,q1))
then consider j being Nat such that
A28: j in dom (MergeSequence (p1,q)) and
A29: (MergeSequence (p1,q)) . j = z by FINSEQ_2:10;
 j in Seg (len (MergeSequence (p1,q))) by A28, FINSEQ_1:def_3;
then A30: j in Seg (len p1) by Def1;
then A31: j in dom (q1 * ((p2 ") * p1)) by A25, FINSEQ_1:def_3;
A32: j in dom p1 by A30, FINSEQ_1:def_3;
then A33: j in dom ((p2 ") * p1) by A21, RELAT_1:27;
then  ((p2 ") * p1) . j in rng ((p2 ") * p1) by FUNCT_1:def_3;
then  ((p2 ") * p1) . j in rng (p2 ") by FUNCT_1:14;
then A34: ((p2 ") * p1) . j in dom p2 by A11, FUNCT_1:33;
then reconsider pj = ((p2 ") * p1) . j as Element of NAT ;
A35: q . j = (q1 * ((p2 ") * p1)) . j by A26, RELAT_1:36
.= q1 . (((p2 ") * p1) . j) by A31, FUNCT_1:12 ;
A36: now__::_thesis:_(MergeSequence_(p2,q1))_._(((p2_")_*_p1)_._j)_=_z
percases ( q . j = TRUE or q . j = FALSE ) by XBOOLEAN:def_3;
supposeA37: q . j = TRUE ; ::_thesis: (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = z
hence (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = p2 . pj by A35, Th5
.= (p2 * ((p2 ") * p1)) . j by A33, FUNCT_1:13
.= ((p2 * (p2 ")) * p1) . j by RELAT_1:36
.= ((id (rng p1)) * p1) . j by A6, A9, A11, FUNCT_1:39
.= p1 . j by RELAT_1:54
.= z by A29, A37, Th5 ;
::_thesis: verum
end;
supposeS: q . j = FALSE ; ::_thesis: (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = z
hence (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = X \ (p2 . pj) by A34, A35, Th6
.= X \ ((p2 * ((p2 ") * p1)) . j) by A33, FUNCT_1:13
.= X \ (((p2 * (p2 ")) * p1) . j) by RELAT_1:36
.= X \ (((id (rng p1)) * p1) . j) by A6, A9, A11, FUNCT_1:39
.= X \ (p1 . j) by RELAT_1:54
.= z by A29, A32, Th6, S ;
::_thesis: verum
end;
end;
end;
 ((p2 ") * p1) . j in Seg (len p2) by A34, FINSEQ_1:def_3;
then  ((p2 ") * p1) . j in Seg (len (MergeSequence (p2,q1))) by Def1;
then  ((p2 ") * p1) . j in dom (MergeSequence (p2,q1)) by FINSEQ_1:def_3;
hence  z in rng (MergeSequence (p2,q1)) by A36, FUNCT_1:def_3; ::_thesis: verum
end;
A39: len q1 = len p2 by A23, FINSEQ_1:6;
 rng (MergeSequence (p2,q1)) c= rng (MergeSequence (p1,q))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (MergeSequence (p2,q1)) or z in rng (MergeSequence (p1,q)) )
assume  z in rng (MergeSequence (p2,q1)) ; ::_thesis: z in rng (MergeSequence (p1,q))
then consider j being Nat such that
A40: j in dom (MergeSequence (p2,q1)) and
A41: (MergeSequence (p2,q1)) . j = z by FINSEQ_2:10;
 j in Seg (len (MergeSequence (p2,q1))) by A40, FINSEQ_1:def_3;
then A42: j in Seg (len p2) by Def1;
then A43: j in dom (q * ((p1 ") * p2)) by A20, FINSEQ_1:def_3;
A44: j in dom p2 by A42, FINSEQ_1:def_3;
then A45: j in dom ((p1 ") * p2) by A18, RELAT_1:27;
then  ((p1 ") * p2) . j in rng ((p1 ") * p2) by FUNCT_1:def_3;
then  ((p1 ") * p2) . j in rng (p1 ") by FUNCT_1:14;
then A46: ((p1 ") * p2) . j in dom p1 by A12, FUNCT_1:33;
then reconsider pj = ((p1 ") * p2) . j as Element of NAT ;
A47: q1 . j = (q * ((p1 ") * p2)) . j by RELAT_1:36
.= q . (((p1 ") * p2) . j) by A43, FUNCT_1:12 ;
A48: now__::_thesis:_(MergeSequence_(p1,q))_._(((p1_")_*_p2)_._j)_=_z
percases ( q1 . j = TRUE or q1 . j = FALSE ) by XBOOLEAN:def_3;
supposeA49: q1 . j = TRUE ; ::_thesis: (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = z
hence (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = p1 . pj by A47, Th5
.= (p1 * ((p1 ") * p2)) . j by A45, FUNCT_1:13
.= ((p1 * (p1 ")) * p2) . j by RELAT_1:36
.= ((id (rng p2)) * p2) . j by A6, A9, A12, FUNCT_1:39
.= p2 . j by RELAT_1:54
.= z by A41, A49, Th5 ;
::_thesis: verum
end;
supposeA50: q1 . j = FALSE ; ::_thesis: (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = z
hence (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = X \ (p1 . pj) by A46, A47, Th6
.= X \ ((p1 * ((p1 ") * p2)) . j) by A45, FUNCT_1:13
.= X \ (((p1 * (p1 ")) * p2) . j) by RELAT_1:36
.= X \ (((id (rng p2)) * p2) . j) by A6, A9, A12, FUNCT_1:39
.= X \ (p2 . j) by RELAT_1:54
.= z by A41, A44, A50, Th6 ;
::_thesis: verum
end;
end;
end;
 ((p1 ") * p2) . j in Seg (len p1) by A46, FINSEQ_1:def_3;
then  ((p1 ") * p2) . j in Seg (len (MergeSequence (p1,q))) by Def1;
then  ((p1 ") * p2) . j in dom (MergeSequence (p1,q)) by FINSEQ_1:def_3;
hence  z in rng (MergeSequence (p1,q)) by A48, FUNCT_1:def_3; ::_thesis: verum
end;
then  P = Intersect (rng (MergeSequence (p2,q1))) by A15, A27, XBOOLE_0:def_10;
hence  P in C2 by A10, A39; ::_thesis: verum
end;
thus  ( P in C2 implies P in C1 ) ::_thesis: verum
proof
 p2 is Function of (dom p2),(rng p2) by FUNCT_2:1;
then A51: p2 " is Function of (rng p2),(dom p2) by A11, FUNCT_2:25;
 p1 is FinSequence of rng p2 by A6, A9, FINSEQ_1:def_4;
then A52: (p2 ") * p1 is FinSequence of dom p2 by A51, FINSEQ_2:32;
assume  P in C2 ; ::_thesis: P in C1
then consider q being FinSequence of BOOLEAN  such that
A53: P = Intersect (rng (MergeSequence (p2,q))) and
A54: len q = len p2 by A10;
A55: dom p2 = Seg (len q) by A54, FINSEQ_1:def_3
.= dom q by FINSEQ_1:def_3 ;
then  q is Function of (dom p2),BOOLEAN by FINSEQ_2:26;
then  q * ((p2 ") * p1) is FinSequence of BOOLEAN by A52, FINSEQ_2:32;
then reconsider q1 = (q * (p2 ")) * p1 as FinSequence of BOOLEAN by RELAT_1:36;
A56: rng p1 = dom (p2 ") by A6, A9, A11, FUNCT_1:33;
then A57: dom ((p2 ") * p1) = dom p1 by RELAT_1:27;
rng ((p2 ") * p1) = rng (p2 ") by A56, RELAT_1:28
.= dom q by A11, A55, FUNCT_1:33 ;
then A58: dom (q * ((p2 ") * p1)) = dom p1 by A57, RELAT_1:27;
A59: rng p2 = dom (p1 ") by A6, A9, A12, FUNCT_1:33;
then A60: dom ((p1 ") * p2) = dom p2 by RELAT_1:27;
A61: Seg (len q1) = dom q1 by FINSEQ_1:def_3
.= dom p1 by A58, RELAT_1:36
.= Seg (len p1) by FINSEQ_1:def_3 ;
then A62: dom p1 = Seg (len q1) by FINSEQ_1:def_3
.= dom q1 by FINSEQ_1:def_3 ;
rng ((p1 ") * p2) = rng (p1 ") by A59, RELAT_1:28
.= dom q1 by A12, A62, FUNCT_1:33 ;
then A63: dom (q1 * ((p1 ") * p2)) = dom p2 by A60, RELAT_1:27;
A64: (q1 * (p1 ")) * p2 = ((q * (p2 ")) * p1) * ((p1 ") * p2) by RELAT_1:36
.= (q * (p2 ")) * (p1 * ((p1 ") * p2)) by RELAT_1:36
.= (q * (p2 ")) * ((p1 * (p1 ")) * p2) by RELAT_1:36
.= (q * (p2 ")) * ((id (rng p1)) * p2) by A12, FUNCT_1:39
.= (q * (p2 ")) * p2 by A6, A9, RELAT_1:54
.= q * ((p2 ") * p2) by RELAT_1:36
.= q * (id (dom p2)) by A11, FUNCT_1:39
.= q by A55, RELAT_1:52 ;
A65: rng (MergeSequence (p2,q)) c= rng (MergeSequence (p1,q1))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (MergeSequence (p2,q)) or z in rng (MergeSequence (p1,q1)) )
assume  z in rng (MergeSequence (p2,q)) ; ::_thesis: z in rng (MergeSequence (p1,q1))
then consider j being Nat such that
A66: j in dom (MergeSequence (p2,q)) and
A67: (MergeSequence (p2,q)) . j = z by FINSEQ_2:10;
 j in Seg (len (MergeSequence (p2,q))) by A66, FINSEQ_1:def_3;
then A68: j in Seg (len p2) by Def1;
then A69: j in dom (q1 * ((p1 ") * p2)) by A63, FINSEQ_1:def_3;
A70: j in dom p2 by A68, FINSEQ_1:def_3;
then A71: j in dom ((p1 ") * p2) by A59, RELAT_1:27;
then  ((p1 ") * p2) . j in rng ((p1 ") * p2) by FUNCT_1:def_3;
then  ((p1 ") * p2) . j in rng (p1 ") by FUNCT_1:14;
then A72: ((p1 ") * p2) . j in dom p1 by A12, FUNCT_1:33;
then reconsider pj = ((p1 ") * p2) . j as Element of NAT ;
A73: q . j = (q1 * ((p1 ") * p2)) . j by A64, RELAT_1:36
.= q1 . (((p1 ") * p2) . j) by A69, FUNCT_1:12 ;
A74: now__::_thesis:_(MergeSequence_(p1,q1))_._(((p1_")_*_p2)_._j)_=_z
percases ( q . j = TRUE or q . j = FALSE ) by XBOOLEAN:def_3;
supposeA75: q . j = TRUE ; ::_thesis: (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = z
hence (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = p1 . pj by A73, Th5
.= (p1 * ((p1 ") * p2)) . j by A71, FUNCT_1:13
.= ((p1 * (p1 ")) * p2) . j by RELAT_1:36
.= ((id (rng p2)) * p2) . j by A6, A9, A12, FUNCT_1:39
.= p2 . j by RELAT_1:54
.= z by A67, A75, Th5 ;
::_thesis: verum
end;
supposeA76: q . j = FALSE ; ::_thesis: (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = z
hence (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = X \ (p1 . pj) by A72, A73, Th6
.= X \ ((p1 * ((p1 ") * p2)) . j) by A71, FUNCT_1:13
.= X \ (((p1 * (p1 ")) * p2) . j) by RELAT_1:36
.= X \ (((id (rng p2)) * p2) . j) by A6, A9, A12, FUNCT_1:39
.= X \ (p2 . j) by RELAT_1:54
.= z by A67, A70, A76, Th6 ;
::_thesis: verum
end;
end;
end;
 ((p1 ") * p2) . j in Seg (len p1) by A72, FINSEQ_1:def_3;
then  ((p1 ") * p2) . j in Seg (len (MergeSequence (p1,q1))) by Def1;
then  ((p1 ") * p2) . j in dom (MergeSequence (p1,q1)) by FINSEQ_1:def_3;
hence  z in rng (MergeSequence (p1,q1)) by A74, FUNCT_1:def_3; ::_thesis: verum
end;
A77: len q1 = len p1 by A61, FINSEQ_1:6;
 rng (MergeSequence (p1,q1)) c= rng (MergeSequence (p2,q))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (MergeSequence (p1,q1)) or z in rng (MergeSequence (p2,q)) )
assume  z in rng (MergeSequence (p1,q1)) ; ::_thesis: z in rng (MergeSequence (p2,q))
then consider j being Nat such that
A78: j in dom (MergeSequence (p1,q1)) and
A79: (MergeSequence (p1,q1)) . j = z by FINSEQ_2:10;
 j in Seg (len (MergeSequence (p1,q1))) by A78, FINSEQ_1:def_3;
then A80: j in Seg (len p1) by Def1;
then A81: j in dom (q * ((p2 ") * p1)) by A58, FINSEQ_1:def_3;
A82: j in dom p1 by A80, FINSEQ_1:def_3;
then A83: j in dom ((p2 ") * p1) by A56, RELAT_1:27;
then  ((p2 ") * p1) . j in rng ((p2 ") * p1) by FUNCT_1:def_3;
then  ((p2 ") * p1) . j in rng (p2 ") by FUNCT_1:14;
then A84: ((p2 ") * p1) . j in dom p2 by A11, FUNCT_1:33;
then reconsider pj = ((p2 ") * p1) . j as Element of NAT ;
A85: q1 . j = (q * ((p2 ") * p1)) . j by RELAT_1:36
.= q . (((p2 ") * p1) . j) by A81, FUNCT_1:12 ;
A86: now__::_thesis:_(MergeSequence_(p2,q))_._(((p2_")_*_p1)_._j)_=_z
percases ( q1 . j = TRUE or q1 . j = FALSE ) by XBOOLEAN:def_3;
supposeA87: q1 . j = TRUE ; ::_thesis: (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = z
hence (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = p2 . pj by A85, Th5
.= (p2 * ((p2 ") * p1)) . j by A83, FUNCT_1:13
.= ((p2 * (p2 ")) * p1) . j by RELAT_1:36
.= ((id (rng p1)) * p1) . j by A6, A9, A11, FUNCT_1:39
.= p1 . j by RELAT_1:54
.= z by A79, A87, Th5 ;
::_thesis: verum
end;
supposeA88: q1 . j = FALSE ; ::_thesis: (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = z
hence (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = X \ (p2 . pj) by A84, A85, Th6
.= X \ ((p2 * ((p2 ") * p1)) . j) by A83, FUNCT_1:13
.= X \ (((p2 * (p2 ")) * p1) . j) by RELAT_1:36
.= X \ (((id (rng p1)) * p1) . j) by A6, A9, A11, FUNCT_1:39
.= X \ (p1 . j) by RELAT_1:54
.= z by A79, A82, A88, Th6 ;
::_thesis: verum
end;
end;
end;
 ((p2 ") * p1) . j in Seg (len p2) by A84, FINSEQ_1:def_3;
then  ((p2 ") * p1) . j in Seg (len (MergeSequence (p2,q))) by Def1;
then  ((p2 ") * p1) . j in dom (MergeSequence (p2,q)) by FINSEQ_1:def_3;
hence  z in rng (MergeSequence (p2,q)) by A86, FUNCT_1:def_3; ::_thesis: verum
end;
then  P = Intersect (rng (MergeSequence (p1,q1))) by A53, A65, XBOOLE_0:def_10;
hence  P in C1 by A7, A77; ::_thesis: verum
end;
end;
hence  C1 = C2 by SETFAM_1:31; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Components YELLOW15:def_2_:_
 for X being set
for Y being finite Subset-Family of X
for b3 being Subset-Family of X holds
( b3 = Components Y iff ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & b3 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) );

registration
let X be set ;
let Y be finite Subset-Family of X;
cluster Components Y ->  finite ;
coherence
 Components Y is finite
proof
consider p being FinSequence of bool X such that
 len p = card Y and
 rng p = Y and
A1: Components Y =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  by Def2;
deffunc H1( Element of BOOLEAN * ) ->  Element of bool X = Intersect (rng (MergeSequence (p,X)));
A2: Components Y c=  {  (Intersect (rng (MergeSequence (p,q)))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Components Y or z in  {  (Intersect (rng (MergeSequence (p,q)))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN  }  )
assume  z in Components Y ; ::_thesis: z in  {  (Intersect (rng (MergeSequence (p,q)))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN  }
then consider q being FinSequence of BOOLEAN  such that
A3: ( z = Intersect (rng (MergeSequence (p,q))) & len q = len p ) by A1;
 ( q is Element of BOOLEAN * & q is Element of (len q) -tuples_on BOOLEAN ) by FINSEQ_1:def_11, FINSEQ_2:92;
hence  z in  {  (Intersect (rng (MergeSequence (p,q)))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN  }  by A3; ::_thesis: verum
end;
A4: (len p) -tuples_on BOOLEAN is finite ;
  {  H1(q) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN  }  is finite from FRAENKEL:sch_21(A4);
hence  Components Y is finite by A2; ::_thesis: verum
end;
end;

theorem Th16: :: YELLOW15:16
for X being set
for Y being empty Subset-Family of X holds Components Y = {X}
proof
let X be set ; ::_thesis: for Y being empty Subset-Family of X holds Components Y = {X}
let Y be empty Subset-Family of X; ::_thesis: Components Y = {X}
consider p being FinSequence of bool X such that
A1: len p = card Y and
A2: rng p = Y and
A3: Components Y =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  by Def2;
thus  Components Y = {X} ::_thesis: verum
proof
thus  Components Y c= {X} :: according to XBOOLE_0:def_10 ::_thesis: {X} c= Components Y
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Components Y or z in {X} )
assume  z in Components Y ; ::_thesis: z in {X}
then consider q being FinSequence of BOOLEAN  such that
A4: z = Intersect (rng (MergeSequence (p,q))) and
 len q = len p by A3;
 p = <*> (bool X) by A2;
then  rng (MergeSequence (p,q)) = {} by Th8, RELAT_1:38;
then  Intersect (rng (MergeSequence (p,q))) = X by SETFAM_1:def_9;
hence  z in {X} by A4, TARSKI:def_1; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {X} or z in Components Y )
 p = <*> (bool X) by A2;
then  rng (MergeSequence (p,(<*> BOOLEAN))) = {} by Th8, RELAT_1:38;
then A5: Intersect (rng (MergeSequence (p,(<*> BOOLEAN)))) = X by SETFAM_1:def_9;
assume  z in {X} ; ::_thesis: z in Components Y
then  z = X by TARSKI:def_1;
hence  z in Components Y by A1, A3, A5; ::_thesis: verum
end;
end;

theorem :: YELLOW15:17
for X being set
for Y, Z being finite Subset-Family of X st Z c= Y holds
Components Y is_finer_than Components Z
proof
let X be set ; ::_thesis: for Y, Z being finite Subset-Family of X st Z c= Y holds
Components Y is_finer_than Components Z
let Y, Z be finite Subset-Family of X; ::_thesis: ( Z c= Y implies Components Y is_finer_than Components Z )
assume A1: Z c= Y ; ::_thesis: Components Y is_finer_than Components Z
now__::_thesis:_for_V_being_set_st_V_in_Components_Y_holds_
ex_W_being_set_st_
(_W_in_Components_Z_&_V_c=_W_)
let V be set ; ::_thesis: ( V in Components Y implies ex W being set st
( W in Components Z & V c= W ) )
consider p being FinSequence of bool X such that
A2: len p = card Y and
A3: rng p = Y and
A4: Components Y =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  by Def2;
consider p1 being FinSequence of bool X such that
 len p1 = card Z and
A5: rng p1 = Z and
A6: Components Z =  {  (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1  }  by Def2;
A7: p1 is FinSequence of rng p by A1, A3, A5, FINSEQ_1:def_4;
assume  V in Components Y ; ::_thesis: ex W being set st
( W in Components Z & V c= W )
then consider q being FinSequence of BOOLEAN  such that
A8: V = Intersect (rng (MergeSequence (p,q))) and
A9: len q = len p by A4;
 dom p = dom q by A9, FINSEQ_3:29;
then A10: q is Function of (dom p),BOOLEAN by FINSEQ_2:26;
A11: p is one-to-one by A2, A3, FINSEQ_4:62;
then A12: rng p1 c= dom (p ") by A1, A3, A5, FUNCT_1:33;
rng (p ") = dom p by A11, FUNCT_1:33
.= dom q by A9, FINSEQ_3:29 ;
then A13: rng ((p ") * p1) c= dom q by RELAT_1:26;
 p is Function of (dom p),(rng p) by FUNCT_2:1;
then  p " is Function of (rng p),(dom p) by A11, FUNCT_2:25;
then  (p ") * p1 is FinSequence of dom p by A7, FINSEQ_2:32;
then  q * ((p ") * p1) is FinSequence of BOOLEAN by A10, FINSEQ_2:32;
then reconsider q1 = (q * (p ")) * p1 as FinSequence of BOOLEAN by RELAT_1:36;
reconsider W = Intersect (rng (MergeSequence (p1,q1))) as set ;
take W = W; ::_thesis: ( W in Components Z & V c= W )
dom q1 = dom (q * ((p ") * p1)) by RELAT_1:36
.= dom ((p ") * p1) by A13, RELAT_1:27
.= dom p1 by A12, RELAT_1:27 ;
then  len q1 = len p1 by FINSEQ_3:29;
hence  W in Components Z by A6; ::_thesis: V c= W
 rng (MergeSequence (p1,q1)) c= rng (MergeSequence (p,q))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (MergeSequence (p1,q1)) or z in rng (MergeSequence (p,q)) )
assume  z in rng (MergeSequence (p1,q1)) ; ::_thesis: z in rng (MergeSequence (p,q))
then consider i being Nat such that
A14: i in dom (MergeSequence (p1,q1)) and
A15: (MergeSequence (p1,q1)) . i = z by FINSEQ_2:10;
A16: i in dom p1 by A14, Th4;
then A17: i in dom ((p ") * p1) by A12, RELAT_1:27;
then  ((p ") * p1) . i in rng ((p ") * p1) by FUNCT_1:def_3;
then A18: ((p ") * p1) . i in rng (p ") by FUNCT_1:14;
then A19: ((p ") * p1) . i in dom p by A11, FUNCT_1:33;
then reconsider j = ((p ") * p1) . i as Element of NAT ;
A20: q . j = (q * ((p ") * p1)) . i by A17, FUNCT_1:13
.= q1 . i by RELAT_1:36 ;
A21: p1 is Function of (dom p1),(rng p) by A1, A3, A5, FUNCT_2:2;
A22: j in dom p by A11, A18, FUNCT_1:33;
A23: now__::_thesis:_(MergeSequence_(p,q))_._j_=_z
percases ( q . j = TRUE or q . j = FALSE ) by XBOOLEAN:def_3;
supposeA24: q . j = TRUE ; ::_thesis: (MergeSequence (p,q)) . j = z
hence (MergeSequence (p,q)) . j = p . j by Th5
.= (p * ((p ") * p1)) . i by A17, FUNCT_1:13
.= ((p * (p ")) * p1) . i by RELAT_1:36
.= ((id (rng p)) * p1) . i by A11, FUNCT_1:39
.= p1 . i by A21, FUNCT_2:17
.= z by A15, A20, A24, Th5 ;
::_thesis: verum
end;
supposeA25: q . j = FALSE ; ::_thesis: (MergeSequence (p,q)) . j = z
hence (MergeSequence (p,q)) . j = X \ (p . j) by A22, Th6
.= X \ ((p * ((p ") * p1)) . i) by A17, FUNCT_1:13
.= X \ (((p * (p ")) * p1) . i) by RELAT_1:36
.= X \ (((id (rng p)) * p1) . i) by A11, FUNCT_1:39
.= X \ (p1 . i) by A21, FUNCT_2:17
.= z by A15, A16, A20, A25, Th6 ;
::_thesis: verum
end;
end;
end;
 j in dom (MergeSequence (p,q)) by A19, Th4;
hence  z in rng (MergeSequence (p,q)) by A23, FUNCT_1:def_3; ::_thesis: verum
end;
hence  V c= W by A8, SETFAM_1:44; ::_thesis: verum
end;
hence  Components Y is_finer_than Components Z by SETFAM_1:def_2; ::_thesis: verum
end;

theorem Th18: :: YELLOW15:18
for X being set
for Y being finite Subset-Family of X holds union (Components Y) = X
proof
let X be set ; ::_thesis: for Y being finite Subset-Family of X holds union (Components Y) = X
let Y be finite Subset-Family of X; ::_thesis: union (Components Y) = X
 X c= union (Components Y)
proof
deffunc H1( set ) ->  Element of BOOLEAN = FALSE ;
deffunc H2( set ) ->  Element of BOOLEAN = TRUE ;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X or z in union (Components Y) )
consider p being FinSequence of bool X such that
 len p = card Y and
 rng p = Y and
A1: Components Y =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  by Def2;
defpred S1[ set ] means z in p . $1;
A2: for i being Nat st i in Seg (len p) holds
( ( S1[i] implies H2(i) in BOOLEAN ) & ( not S1[i] implies H1(i) in BOOLEAN ) ) ;
consider q being FinSequence of BOOLEAN  such that
A3: len q = len p and
A4: for i being Nat st i in Seg (len p) holds
( ( S1[i] implies q . i = H2(i) ) & ( not S1[i] implies q . i = H1(i) ) ) from YELLOW15:sch_1(A2);
assume A5: z in X ; ::_thesis: z in union (Components Y)
now__::_thesis:_for_Z_being_set_st_Z_in_rng_(MergeSequence_(p,q))_holds_
z_in_Z
let Z be set ; ::_thesis: ( Z in rng (MergeSequence (p,q)) implies z in Z )
assume  Z in rng (MergeSequence (p,q)) ; ::_thesis: z in Z
then consider i being Nat such that
A6: i in dom (MergeSequence (p,q)) and
A7: (MergeSequence (p,q)) . i = Z by FINSEQ_2:10;
A8: dom (MergeSequence (p,q)) = dom p by Th4;
then A9: dom (MergeSequence (p,q)) = Seg (len p) by FINSEQ_1:def_3;
now__::_thesis:_z_in_Z
percases ( z in p . i or not z in p . i ) ;
supposeA10: z in p . i ; ::_thesis: z in Z
then  q . i = TRUE by A4, A6, A9;
hence  z in Z by A7, A10, Th5; ::_thesis: verum
end;
supposeA11: not z in p . i ; ::_thesis: z in Z
then  q . i = FALSE by A4, A6, A9;
then  (MergeSequence (p,q)) . i = X \ (p . i) by A6, A8, Th6;
hence  z in Z by A5, A7, A11, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
hence  z in Z ; ::_thesis: verum
end;
then A12: z in Intersect (rng (MergeSequence (p,q))) by A5, SETFAM_1:43;
 Intersect (rng (MergeSequence (p,q))) in Components Y by A1, A3;
hence  z in union (Components Y) by A12, TARSKI:def_4; ::_thesis: verum
end;
hence  union (Components Y) = X by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th19: :: YELLOW15:19
for X being set
for Y being finite Subset-Family of X
for A, B being set st A in Components Y & B in Components Y & A <> B holds
A misses B
proof
let X be set ; ::_thesis: for Y being finite Subset-Family of X
for A, B being set st A in Components Y & B in Components Y & A <> B holds
A misses B
let Y be finite Subset-Family of X; ::_thesis: for A, B being set st A in Components Y & B in Components Y & A <> B holds
A misses B
let A, B be set ; ::_thesis: ( A in Components Y & B in Components Y & A <> B implies A misses B )
assume that
A1: A in Components Y and
A2: B in Components Y and
A3: A <> B ; ::_thesis: A misses B
assume  A /\ B <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider z being set  such that
A4: z in A /\ B by XBOOLE_0:def_1;
A5: z in B by A4, XBOOLE_0:def_4;
A6: z in A by A4, XBOOLE_0:def_4;
consider p being FinSequence of bool X such that
 len p = card Y and
 rng p = Y and
A7: Components Y =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  by Def2;
consider q1 being FinSequence of BOOLEAN  such that
A8: A = Intersect (rng (MergeSequence (p,q1))) and
 len q1 = len p by A1, A7;
consider q2 being FinSequence of BOOLEAN  such that
A9: B = Intersect (rng (MergeSequence (p,q2))) and
 len q2 = len p by A2, A7;
A10: len (MergeSequence (p,q1)) = len p by Def1;
then A11: dom (MergeSequence (p,q1)) = Seg (len p) by FINSEQ_1:def_3;
A12: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(MergeSequence_(p,q1))_holds_
(MergeSequence_(p,q1))_._i_=_(MergeSequence_(p,q2))_._i
let i be Nat; ::_thesis: ( i in dom (MergeSequence (p,q1)) implies (MergeSequence (p,q1)) . b1 = (MergeSequence (p,q2)) . b1 )
assume A13: i in dom (MergeSequence (p,q1)) ; ::_thesis: (MergeSequence (p,q1)) . b1 = (MergeSequence (p,q2)) . b1
then A14: i in dom p by A11, FINSEQ_1:def_3;
 (MergeSequence (p,q1)) . i in rng (MergeSequence (p,q1)) by A13, FUNCT_1:def_3;
then A15: z in (MergeSequence (p,q1)) . i by A8, A6, SETFAM_1:43;
 i in dom (MergeSequence (p,q2)) by A14, Th4;
then  (MergeSequence (p,q2)) . i in rng (MergeSequence (p,q2)) by FUNCT_1:def_3;
then A16: z in (MergeSequence (p,q2)) . i by A9, A5, SETFAM_1:43;
percases ( q1 . i = TRUE or q1 . i = FALSE ) by XBOOLEAN:def_3;
suppose q1 . i = TRUE ; ::_thesis: (MergeSequence (p,q1)) . b1 = (MergeSequence (p,q2)) . b1
then A17: (MergeSequence (p,q1)) . i = p . i by Th5;
 q2 . i = TRUE
proof
assume  not q2 . i = TRUE ; ::_thesis: contradiction
then  (MergeSequence (p,q2)) . i = X \ (p . i) by A14, Th6, XBOOLEAN:def_3;
hence  contradiction by A15, A16, A17, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  (MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i by A17, Th5; ::_thesis: verum
end;
suppose q1 . i = FALSE ; ::_thesis: (MergeSequence (p,q1)) . b1 = (MergeSequence (p,q2)) . b1
then A18: (MergeSequence (p,q1)) . i = X \ (p . i) by A14, Th6;
 q2 . i = FALSE
proof
assume  not q2 . i = FALSE ; ::_thesis: contradiction
then  q2 . i = TRUE by XBOOLEAN:def_3;
then  (MergeSequence (p,q2)) . i = p . i by Th5;
hence  contradiction by A15, A16, A18, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  (MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i by A14, A18, Th6; ::_thesis: verum
end;
end;
end;
 len (MergeSequence (p,q2)) = len p by Def1;
hence  contradiction by A3, A8, A9, A10, A12, FINSEQ_2:9; ::_thesis: verum
end;

definition
let X be set ;
let Y be finite Subset-Family of X;
attrY is in_general_position  means :Def3: :: YELLOW15:def 3
 not {} in Components Y;
end;

:: deftheorem Def3 defines in_general_position YELLOW15:def_3_:_
 for X being set
for Y being finite Subset-Family of X holds
( Y is in_general_position iff not {} in Components Y );

theorem :: YELLOW15:20
for X being set
for Y, Z being finite Subset-Family of X st Z is in_general_position & Y c= Z holds
Y is in_general_position
proof
let X be set ; ::_thesis: for Y, Z being finite Subset-Family of X st Z is in_general_position & Y c= Z holds
Y is in_general_position
let Y, Z be finite Subset-Family of X; ::_thesis: ( Z is in_general_position & Y c= Z implies Y is in_general_position )
assume that
A1: Z is in_general_position and
A2: Y c= Z ; ::_thesis: Y is in_general_position
A3: not {} in Components Z by A1, Def3;
 not {} in Components Y
proof
deffunc H1( set ) ->  Element of BOOLEAN = TRUE ;
consider p being FinSequence of bool X such that
A4: len p = card Y and
A5: rng p = Y and
A6: Components Y =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  by Def2;
A7: p is one-to-one by A4, A5, FINSEQ_4:62;
then A8: rng p = dom (p ") by FUNCT_1:33;
consider p1 being FinSequence of bool X such that
A9: len p1 = card Z and
A10: rng p1 = Z and
A11: Components Z =  {  (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1  }  by Def2;
defpred S1[ set ] means p1 . $1 in rng p;
assume  {} in Components Y ; ::_thesis: contradiction
then consider q being FinSequence of BOOLEAN  such that
A12: {} = Intersect (rng (MergeSequence (p,q))) and
A13: len q = len p by A6;
deffunc H2( set ) ->  set = ((q * (p ")) * p1) . $1;
A14: dom p = rng (p ") by A7, FUNCT_1:33;
A15: for i being Nat st i in Seg (len p1) holds
( ( S1[i] implies H2(i) in BOOLEAN ) & ( not S1[i] implies H1(i) in BOOLEAN ) )
proof
let i be Nat; ::_thesis: ( i in Seg (len p1) implies ( ( S1[i] implies H2(i) in BOOLEAN ) & ( not S1[i] implies H1(i) in BOOLEAN ) ) )
assume  i in Seg (len p1) ; ::_thesis: ( ( S1[i] implies H2(i) in BOOLEAN ) & ( not S1[i] implies H1(i) in BOOLEAN ) )
then A16: i in dom p1 by FINSEQ_1:def_3;
thus  ( p1 . i in rng p implies ((q * (p ")) * p1) . i in BOOLEAN ) ::_thesis: ( not S1[i] implies H1(i) in BOOLEAN )
proof
assume A17: p1 . i in rng p ; ::_thesis: ((q * (p ")) * p1) . i in BOOLEAN
 rng (p ") = dom q by A13, A14, FINSEQ_3:29;
then  p1 . i in dom (q * (p ")) by A8, A17, RELAT_1:27;
then A18: (q * (p ")) . (p1 . i) in rng (q * (p ")) by FUNCT_1:def_3;
 dom (q * (p ")) c= rng p by A8, RELAT_1:25;
then  rng (q * (p ")) = rng ((q * (p ")) * p1) by A2, A5, A10, RELAT_1:28, XBOOLE_1:1;
then  ((q * (p ")) * p1) . i in rng ((q * (p ")) * p1) by A16, A18, FUNCT_1:13;
hence  ((q * (p ")) * p1) . i in BOOLEAN ; ::_thesis: verum
end;
thus  ( not S1[i] implies H1(i) in BOOLEAN ) ; ::_thesis: verum
end;
consider q1 being FinSequence of BOOLEAN  such that
A19: len q1 = len p1 and
A20: for i being Nat st i in Seg (len p1) holds
( ( S1[i] implies q1 . i = H2(i) ) & ( not S1[i] implies q1 . i = H1(i) ) ) from YELLOW15:sch_1(A15);
A21: p1 is one-to-one by A9, A10, FINSEQ_4:62;
then A22: rng p1 = dom (p1 ") by FUNCT_1:33;
 rng (MergeSequence (p,q)) c= rng (MergeSequence (p1,q1))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (MergeSequence (p,q)) or z in rng (MergeSequence (p1,q1)) )
assume  z in rng (MergeSequence (p,q)) ; ::_thesis: z in rng (MergeSequence (p1,q1))
then consider i being Nat such that
A23: i in dom (MergeSequence (p,q)) and
A24: (MergeSequence (p,q)) . i = z by FINSEQ_2:10;
 i in Seg (len (MergeSequence (p,q))) by A23, FINSEQ_1:def_3;
then  i in Seg (len p) by Def1;
then A25: i in dom p by FINSEQ_1:def_3;
then A26: i in dom ((p1 ") * p) by A2, A5, A10, A22, RELAT_1:27;
then  ((p1 ") * p) . i in rng ((p1 ") * p) by FUNCT_1:def_3;
then A27: ((p1 ") * p) . i in rng (p1 ") by FUNCT_1:14;
then A28: ((p1 ") * p) . i in dom p1 by A21, FUNCT_1:33;
then reconsider j = ((p1 ") * p) . i as Element of NAT ;
p1 . j = (p1 * ((p1 ") * p)) . i by A26, FUNCT_1:13
.= ((p1 * (p1 ")) * p) . i by RELAT_1:36
.= ((id (rng p1)) * p) . i by A21, FUNCT_1:39
.= p . i by A2, A5, A10, RELAT_1:53 ;
then A29: p1 . j in rng p by A25, FUNCT_1:def_3;
 j in Seg (len p1) by A28, FINSEQ_1:def_3;
then A30: q1 . j = ((q * (p ")) * p1) . (((p1 ") * p) . i) by A20, A29
.= (((q * (p ")) * p1) * ((p1 ") * p)) . i by A26, FUNCT_1:13
.= ((q * (p ")) * (p1 * ((p1 ") * p))) . i by RELAT_1:36
.= ((q * (p ")) * ((p1 * (p1 ")) * p)) . i by RELAT_1:36
.= ((q * (p ")) * ((id (rng p1)) * p)) . i by A21, FUNCT_1:39
.= ((q * (p ")) * p) . i by A2, A5, A10, RELAT_1:53
.= (q * ((p ") * p)) . i by RELAT_1:36
.= (q * (id (dom p))) . i by A7, FUNCT_1:39
.= (q * (id (dom q))) . i by A13, FINSEQ_3:29
.= q . i by RELAT_1:52 ;
A31: j in dom p1 by A21, A27, FUNCT_1:33;
A32: now__::_thesis:_z_=_(MergeSequence_(p1,q1))_._j
percases ( q . i = TRUE or q . i = FALSE ) by XBOOLEAN:def_3;
supposeA33: q . i = TRUE ; ::_thesis: z = (MergeSequence (p1,q1)) . j
hence z = p . i by A24, Th5
.= ((id (rng p1)) * p) . i by A2, A5, A10, RELAT_1:53
.= ((p1 * (p1 ")) * p) . i by A21, FUNCT_1:39
.= (p1 * ((p1 ") * p)) . i by RELAT_1:36
.= p1 . j by A26, FUNCT_1:13
.= (MergeSequence (p1,q1)) . j by A30, A33, Th5 ;
::_thesis: verum
end;
supposeA34: q . i = FALSE ; ::_thesis: z = (MergeSequence (p1,q1)) . j
hence z = X \ (p . i) by A24, A25, Th6
.= X \ (((id (rng p1)) * p) . i) by A2, A5, A10, RELAT_1:53
.= X \ (((p1 * (p1 ")) * p) . i) by A21, FUNCT_1:39
.= X \ ((p1 * ((p1 ") * p)) . i) by RELAT_1:36
.= X \ (p1 . j) by A26, FUNCT_1:13
.= (MergeSequence (p1,q1)) . j by A31, A30, A34, Th6 ;
::_thesis: verum
end;
end;
end;
 j in dom (MergeSequence (p1,q1)) by A28, Th4;
hence  z in rng (MergeSequence (p1,q1)) by A32, FUNCT_1:def_3; ::_thesis: verum
end;
then  {} = Intersect (rng (MergeSequence (p1,q1))) by A12, SETFAM_1:44, XBOOLE_1:3;
hence  contradiction by A3, A11, A19; ::_thesis: verum
end;
hence  Y is in_general_position by Def3; ::_thesis: verum
end;

theorem :: YELLOW15:21
for X being non empty set
for Y being empty Subset-Family of X holds Y is in_general_position
proof
let X be non empty set ; ::_thesis: for Y being empty Subset-Family of X holds Y is in_general_position
let Y be empty Subset-Family of X; ::_thesis: Y is in_general_position
 not {} in {X} by TARSKI:def_1;
then  not {} in Components Y by Th16;
hence  Y is in_general_position by Def3; ::_thesis: verum
end;

theorem :: YELLOW15:22
for X being non empty set
for Y being finite Subset-Family of X st Y is in_general_position holds
Components Y is a_partition of X
proof
let X be non empty set ; ::_thesis: for Y being finite Subset-Family of X st Y is in_general_position holds
Components Y is a_partition of X
let Y be finite Subset-Family of X; ::_thesis: ( Y is in_general_position implies Components Y is a_partition of X )
assume  Y is in_general_position ; ::_thesis: Components Y is a_partition of X
then A1: for A being Subset of X st A in Components Y holds
( A <> {} & ( for B being Subset of X holds
( not B in Components Y or A = B or A misses B ) ) ) by Def3, Th19;
 union (Components Y) = X by Th18;
hence  Components Y is a_partition of X by A1, EQREL_1:def_4; ::_thesis: verum
end;

begin

theorem Th23: :: YELLOW15:23
for L being non empty RelStr holds
( [#] L is infs-closed & [#] L is sups-closed )
proof
let L be non empty RelStr ; ::_thesis: ( [#] L is infs-closed & [#] L is sups-closed )
 for X being Subset of ([#] L) st ex_inf_of X,L holds
"/\" (X,L) in [#] L ;
hence  [#] L is infs-closed by WAYBEL23:19; ::_thesis: [#] L is sups-closed
 for X being Subset of ([#] L) st ex_sup_of X,L holds
"\/" (X,L) in [#] L ;
hence  [#] L is sups-closed by WAYBEL23:20; ::_thesis: verum
end;

theorem Th24: :: YELLOW15:24
for L being non empty RelStr holds
( [#] L is with_bottom & [#] L is with_top )
proof
let L be non empty RelStr ; ::_thesis: ( [#] L is with_bottom & [#] L is with_top )
 Bottom L in [#] L ;
hence  [#] L is with_bottom by WAYBEL23:def_8; ::_thesis: [#] L is with_top
 Top L in [#] L ;
hence  [#] L is with_top by WAYBEL23:def_9; ::_thesis: verum
end;

registration
let L be non empty RelStr ;
cluster [#] L ->  infs-closed sups-closed with_bottom with_top ;
coherence
 ( [#] L is infs-closed & [#] L is sups-closed & [#] L is with_bottom & [#] L is with_top ) by Th23, Th24;
end;

theorem :: YELLOW15:25
for L being continuous sup-Semilattice holds [#] L is CLbasis of L
proof
let L be continuous sup-Semilattice; ::_thesis: [#] L is CLbasis of L
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_((waybelow_x)_/\_([#]_L))
let x be Element of L; ::_thesis: x = sup ((waybelow x) /\ ([#] L))
 (waybelow x) /\ ([#] L) = waybelow x by XBOOLE_1:28;
hence  x = sup ((waybelow x) /\ ([#] L)) by WAYBEL_3:def_5; ::_thesis: verum
end;
hence  [#] L is CLbasis of L by WAYBEL23:def_7; ::_thesis: verum
end;

theorem :: YELLOW15:26
for L being non empty up-complete Poset st L is finite holds
the carrier of L = the carrier of (CompactSublatt L)
proof
let L be non empty up-complete Poset; ::_thesis: ( L is finite implies the carrier of L = the carrier of (CompactSublatt L) )
assume A1: L is finite ; ::_thesis: the carrier of L = the carrier of (CompactSublatt L)
A2: the carrier of L c= the carrier of (CompactSublatt L)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the carrier of L or z in the carrier of (CompactSublatt L) )
assume  z in the carrier of L ; ::_thesis: z in the carrier of (CompactSublatt L)
then reconsider z1 = z as Element of L ;
 z1 is compact by A1, WAYBEL_3:17;
hence  z in the carrier of (CompactSublatt L) by WAYBEL_8:def_1; ::_thesis: verum
end;
 the carrier of (CompactSublatt L) c= the carrier of L by YELLOW_0:def_13;
hence  the carrier of L = the carrier of (CompactSublatt L) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: YELLOW15:27
for L being lower-bounded sup-Semilattice
for B being Subset of L st B is infinite holds
card B = card (finsups B)
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for B being Subset of L st B is infinite holds
card B = card (finsups B)
let B be Subset of L; ::_thesis: ( B is infinite implies card B = card (finsups B) )
defpred S1[ Function, set ] means $2 = "\/" ((rng $1),L);
assume A1: B is infinite ; ::_thesis: card B = card (finsups B)
then reconsider B1 = B as non empty Subset of L ;
A2: for p being Element of B1 * ex u being Element of finsups B1 st S1[p,u]
proof
let p be Element of B1 * ; ::_thesis: ex u being Element of finsups B1 st S1[p,u]
A3: rng p c= the carrier of L by XBOOLE_1:1;
now__::_thesis:_ex_sup_of_rng_p,L
percases ( rng p is empty or not rng p is empty ) ;
suppose rng p is empty ; ::_thesis: ex_sup_of rng p,L
hence  ex_sup_of rng p,L by YELLOW_0:42; ::_thesis: verum
end;
suppose not rng p is empty ; ::_thesis: ex_sup_of rng p,L
hence  ex_sup_of rng p,L by A3, YELLOW_0:54; ::_thesis: verum
end;
end;
end;
then  "\/" ((rng p),L) in  {  ("\/" (Y,L)) where Y is finite Subset of B1 : ex_sup_of Y,L  }  ;
then reconsider u = "\/" ((rng p),L) as Element of finsups B1 by WAYBEL_0:def_27;
take  u ; ::_thesis: S1[p,u]
thus  S1[p,u] ; ::_thesis: verum
end;
consider f being Function of (B1 *),(finsups B1) such that
A4: for p being Element of B1 * holds S1[p,f . p] from FUNCT_2:sch_3(A2);
 B c= finsups B
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in B or z in finsups B )
assume A5: z in B ; ::_thesis: z in finsups B
then reconsider z1 = z as Element of L ;
A6: {z1} c= B
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in {z1} or v in B )
assume  v in {z1} ; ::_thesis: v in B
hence  v in B by A5, TARSKI:def_1; ::_thesis: verum
end;
 ( ex_sup_of {z1},L & z = sup {z1} ) by YELLOW_0:38, YELLOW_0:39;
then  z1 in  {  ("\/" (Y,L)) where Y is finite Subset of B : ex_sup_of Y,L  }  by A6;
hence  z in finsups B by WAYBEL_0:def_27; ::_thesis: verum
end;
then A7: card B c= card (finsups B) by CARD_1:11;
A8: dom f = B1 * by FUNCT_2:def_1;
 finsups B c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in finsups B or z in rng f )
assume  z in finsups B ; ::_thesis: z in rng f
then  z in  {  ("\/" (Y,L)) where Y is finite Subset of B : ex_sup_of Y,L  }  by WAYBEL_0:def_27;
then consider Y being finite Subset of B such that
A9: z = "\/" (Y,L) and
 ex_sup_of Y,L ;
consider p being FinSequence such that
A10: rng p = Y by FINSEQ_1:52;
reconsider p = p as FinSequence of B1 by A10, FINSEQ_1:def_4;
reconsider p1 = p as Element of B1 * by FINSEQ_1:def_11;
 f . p1 = "\/" ((rng p1),L) by A4;
hence  z in rng f by A8, A9, A10, FUNCT_1:def_3; ::_thesis: verum
end;
then  card (finsups B1) c= card (B1 *) by A8, CARD_1:12;
then  card (finsups B1) c= card B1 by A1, CARD_4:24;
hence  card B = card (finsups B) by A7, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: YELLOW15:28
for T being non empty T_0 TopSpace holds card the carrier of T c= card the topology of T
proof
let T be non empty T_0 TopSpace; ::_thesis: card the carrier of T c= card the topology of T
defpred S1[ Element of T, set ] means $2 = ([#] T) \ (Cl {$1});
A1: for e being Element of T ex u being Element of the topology of T st S1[e,u]
proof
let e be Element of T; ::_thesis: ex u being Element of the topology of T st S1[e,u]
reconsider u = ([#] T) \ (Cl {e}) as Element of the topology of T by PRE_TOPC:def_2, PRE_TOPC:def_3;
take  u ; ::_thesis: S1[e,u]
thus  S1[e,u] ; ::_thesis: verum
end;
consider f being Function of the carrier of T, the topology of T such that
A2: for e being Element of T holds S1[e,f . e] from FUNCT_2:sch_3(A1);
A3: f is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A4: ( x1 in dom f & x2 in dom f ) and
A5: f . x1 = f . x2 ; ::_thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of T by A4;
(Cl {y1}) ` = ([#] T) \ (Cl {y1}) by SUBSET_1:def_4
.= f . x2 by A2, A5
.= ([#] T) \ (Cl {y2}) by A2
.= (Cl {y2}) ` by SUBSET_1:def_4 ;
then  ( Cl {y2} c= Cl {y1} & Cl {y1} c= Cl {y2} ) by SUBSET_1:12;
hence  x1 = x2 by YELLOW_8:23, XBOOLE_0:def_10; ::_thesis: verum
end;
 ( dom f = the carrier of T & rng f c= the topology of T ) by FUNCT_2:def_1;
hence  card the carrier of T c= card the topology of T by A3, CARD_1:10; ::_thesis: verum
end;

theorem Th29: :: YELLOW15:29
for T being TopStruct
for X being Subset of T st X is open holds
for B being finite Subset-Family of T st B is Basis of T holds
for Y being set holds
( not Y in Components B or X misses Y or Y c= X )
proof
let T be TopStruct ; ::_thesis: for X being Subset of T st X is open holds
for B being finite Subset-Family of T st B is Basis of T holds
for Y being set holds
( not Y in Components B or X misses Y or Y c= X )
let X be Subset of T; ::_thesis: ( X is open implies for B being finite Subset-Family of T st B is Basis of T holds
for Y being set holds
( not Y in Components B or X misses Y or Y c= X ) )
assume  X is open ; ::_thesis: for B being finite Subset-Family of T st B is Basis of T holds
for Y being set holds
( not Y in Components B or X misses Y or Y c= X )
then A1: X in the topology of T by PRE_TOPC:def_2;
let B be finite Subset-Family of T; ::_thesis: ( B is Basis of T implies for Y being set holds
( not Y in Components B or X misses Y or Y c= X ) )
assume  B is Basis of T ; ::_thesis: for Y being set holds
( not Y in Components B or X misses Y or Y c= X )
then  the topology of T c= UniCl B by CANTOR_1:def_2;
then consider Z being Subset-Family of T such that
A2: Z c= B and
A3: X = union Z by A1, CANTOR_1:def_1;
let Y be set ; ::_thesis: ( not Y in Components B or X misses Y or Y c= X )
consider p being FinSequence of bool the carrier of T such that
 len p = card B and
A4: rng p = B and
A5: Components B =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  by Def2;
assume  Y in Components B ; ::_thesis: ( X misses Y or Y c= X )
then consider q being FinSequence of BOOLEAN  such that
A6: Y = Intersect (rng (MergeSequence (p,q))) and
 len q = len p by A5;
assume  X /\ Y <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: Y c= X
then consider x being set  such that
A7: x in X /\ Y by XBOOLE_0:def_1;
 x in X by A7, XBOOLE_0:def_4;
then consider b being set  such that
A8: x in b and
A9: b in Z by A3, TARSKI:def_4;
A10: x in Y by A7, XBOOLE_0:def_4;
A11: Y c= b
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Y or z in b )
consider i being Nat such that
A12: i in dom p and
A13: p . i = b by A4, A2, A9, FINSEQ_2:10;
A14: i in dom (MergeSequence (p,q)) by A12, Th4;
now__::_thesis:_(MergeSequence_(p,q))_._i_=_b
percases ( q . i = TRUE or q . i = FALSE ) by XBOOLEAN:def_3;
suppose q . i = TRUE ; ::_thesis: (MergeSequence (p,q)) . i = b
hence  (MergeSequence (p,q)) . i = b by A13, Th5; ::_thesis: verum
end;
suppose q . i = FALSE ; ::_thesis: (MergeSequence (p,q)) . i = b
then A15: (MergeSequence (p,q)) . i = the carrier of T \ b by A12, A13, Th6;
 (MergeSequence (p,q)) . i in rng (MergeSequence (p,q)) by A14, FUNCT_1:def_3;
then  Y c= the carrier of T \ b by A6, A15, MSSUBFAM:2;
hence  (MergeSequence (p,q)) . i = b by A10, A8, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
then A16: b in rng (MergeSequence (p,q)) by A14, FUNCT_1:def_3;
assume  z in Y ; ::_thesis: z in b
hence  z in b by A6, A16, SETFAM_1:43; ::_thesis: verum
end;
 b c= X by A3, A9, ZFMISC_1:74;
hence  Y c= X by A11, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: YELLOW15:30
for T being T_0 TopSpace st T is infinite holds
for B being Basis of T holds B is infinite
proof
let T be T_0 TopSpace; ::_thesis: ( T is infinite implies for B being Basis of T holds B is infinite )
assume A1: T is infinite ; ::_thesis: for B being Basis of T holds B is infinite
let B be Basis of T; ::_thesis: B is infinite
assume  B is finite ; ::_thesis: contradiction
then reconsider B1 = B as finite Subset-Family of T ;
 union (Components B1) = the carrier of T by Th18;
then consider X being set  such that
A2: X in Components B1 and
A3: X is infinite by A1, FINSET_1:7;
reconsider X = X as infinite set by A3;
consider x being set  such that
A4: x in X by XBOOLE_0:def_1;
consider y being set  such that
A5: y in X and
A6: x <> y by A4, SUBSET_1:48;
reconsider x1 = x, y1 = y as Element of T by A2, A4, A5;
consider Y being Subset of T such that
A7: Y is open and
A8: ( ( x1 in Y & not y1 in Y ) or ( y1 in Y & not x1 in Y ) ) by A1, A6, T_0TOPSP:def_7;
now__::_thesis:_contradiction
percases ( ( x in Y & not y in Y ) or ( y in Y & not x in Y ) ) by A8;
supposeA9: ( x in Y & not y in Y ) ; ::_thesis: contradiction
then  x in Y /\ X by A4, XBOOLE_0:def_4;
then  X c= Y by A2, A7, Th29, XBOOLE_0:4;
hence  contradiction by A5, A9; ::_thesis: verum
end;
supposeA10: ( y in Y & not x in Y ) ; ::_thesis: contradiction
then  y in Y /\ X by A5, XBOOLE_0:def_4;
then  X c= Y by A2, A7, Th29, XBOOLE_0:4;
hence  contradiction by A4, A10; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem :: YELLOW15:31
for T being non empty TopSpace st T is finite holds
for B being Basis of T
for x being Element of T holds meet  {  A where A is Element of the topology of T : x in A  }  in B
proof
deffunc H1( set ) ->  set = $1;
let T be non empty TopSpace; ::_thesis: ( T is finite implies for B being Basis of T
for x being Element of T holds meet  {  A where A is Element of the topology of T : x in A  }  in B )
assume  T is finite ; ::_thesis: for B being Basis of T
for x being Element of T holds meet  {  A where A is Element of the topology of T : x in A  }  in B
then reconsider tT = the topology of T as non empty finite set ;
let B be Basis of T; ::_thesis: for x being Element of T holds meet  {  A where A is Element of the topology of T : x in A  }  in B
let x be Element of T; ::_thesis: meet  {  A where A is Element of the topology of T : x in A  }  in B
defpred S1[ set ] means x in $1;
  {  A where A is Element of the topology of T : x in A  }  c= bool the carrier of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  A where A is Element of the topology of T : x in A  }  or z in bool the carrier of T )
assume  z in  {  A where A is Element of the topology of T : x in A  }  ; ::_thesis: z in bool the carrier of T
then  ex A being Element of the topology of T st
( z = A & x in A ) ;
hence  z in bool the carrier of T ; ::_thesis: verum
end;
then reconsider sfA =  {  A where A is Element of the topology of T : x in A  }  as Subset-Family of T ;
reconsider sfA = sfA as Subset-Family of T ;
A1: now__::_thesis:_for_Y_being_set_st_Y_in_sfA_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in sfA implies x in Y )
assume  Y in sfA ; ::_thesis: x in Y
then  ex A being Element of the topology of T st
( Y = A & x in A ) ;
hence  x in Y ; ::_thesis: verum
end;
 the carrier of T is Element of the topology of T by PRE_TOPC:def_1;
then  the carrier of T in sfA ;
then A2: x in meet sfA by A1, SETFAM_1:def_1;
B3: now__::_thesis:_for_P_being_Subset_of_T_st_P_in_sfA_holds_
P_is_open
let P be Subset of T; ::_thesis: ( P in sfA implies P is open )
assume  P in sfA ; ::_thesis: P is open
then  ex A being Element of the topology of T st
( P = A & x in A ) ;
hence  P is open by PRE_TOPC:def_2; ::_thesis: verum
end;
  {  H1(A) where A is Element of tT : S1[A]  }  is finite from PRE_CIRC:sch_1();
then  meet sfA is open by B3, TOPS_2:20, TOPS_2:def_1;
then consider a being Subset of T such that
A4: a in B and
A5: x in a and
A6: a c= meet sfA by A2, YELLOW_9:31;
 meet sfA c= a
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet sfA or z in a )
 B c= the topology of T by TOPS_2:64;
then  a in sfA by A4, A5;
hence  ( not z in meet sfA or z in a ) by SETFAM_1:def_1; ::_thesis: verum
end;
hence  meet  {  A where A is Element of the topology of T : x in A  }  in B by A4, A6, XBOOLE_0:def_10; ::_thesis: verum
end;