let S be non empty set ; :: thesis: for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for g being Assign of (BASSModel (R,BASSIGN))
for s0 being Element of S st s0 |= g & ( for s being Element of S st s |= g holds
s |= EX g ) holds
ex pai being inf_path of R st
( pai . 0 = s0 & ( for n being Nat holds pai . (In (n,NAT)) |= g ) )
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for g being Assign of (BASSModel (R,BASSIGN))
for s0 being Element of S st s0 |= g & ( for s being Element of S st s |= g holds
s |= EX g ) holds
ex pai being inf_path of R st
( pai . 0 = s0 & ( for n being Nat holds pai . (In (n,NAT)) |= g ) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for g being Assign of (BASSModel (R,BASSIGN))
for s0 being Element of S st s0 |= g & ( for s being Element of S st s |= g holds
s |= EX g ) holds
ex pai being inf_path of R st
( pai . 0 = s0 & ( for n being Nat holds pai . (In (n,NAT)) |= g ) )
let g be Assign of (BASSModel (R,BASSIGN)); :: thesis: for s0 being Element of S st s0 |= g & ( for s being Element of S st s |= g holds
s |= EX g ) holds
ex pai being inf_path of R st
( pai . 0 = s0 & ( for n being Nat holds pai . (In (n,NAT)) |= g ) )
let s0 be Element of S; :: thesis: ( s0 |= g & ( for s being Element of S st s |= g holds
s |= EX g ) implies ex pai being inf_path of R st
( pai . 0 = s0 & ( for n being Nat holds pai . (In (n,NAT)) |= g ) ) )
assume A1: s0 |= g ; :: thesis: ( ex s being Element of S st
( s |= g & not s |= EX g ) or ex pai being inf_path of R st
( pai . 0 = s0 & ( for n being Nat holds pai . (In (n,NAT)) |= g ) ) )
deffunc H₁( object ) -> set = { x where x is Element of S : [$1,x] in R } ;
assume A2: for s being Element of S st s |= g holds
s |= EX g ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s0 & ( for n being Nat holds pai . (In (n,NAT)) |= g ) )
for p being set st p in BOOL S holds
p <> {} by ORDERS_1:1;
then consider Choice being Function such that
A3: dom Choice = BOOL S and
A4: for p being set st p in BOOL S holds
Choice . p in p by FUNCT_1:111;
deffunc H₂( object ) -> set = UnivF ((H₁($1) /\ (SIGMA g)),Choice,s0);
A5: for x being object st x in S holds
H₂(x) in S

proof

let x be object ; :: thesis: ( x in S implies H₂(x) in S )
assume x in S ; :: thesis: H₂(x) in S
set Y = H₁(x) /\ (SIGMA g);

per cases ( H₁(x) /\ (SIGMA g) in dom Choice or not H₁(x) /\ (SIGMA g) in dom Choice ) ;

suppose A6: H₁(x) /\ (SIGMA g) in dom Choice ; :: thesis: H₂(x) in S

then H₂(x) = Choice . (H₁(x) /\ (SIGMA g)) by Def3;
then H₂(x) in H₁(x) /\ (SIGMA g) by A3, A4, A6;
then H₂(x) in H₁(x) by XBOOLE_0:def 4;
then ex z being Element of S st
( z = H₂(x) & [x,z] in R ) ;
hence H₂(x) in S ; :: thesis: verum

end;

suppose not H₁(x) /\ (SIGMA g) in dom Choice ; :: thesis: H₂(x) in S

then H₂(x) = s0 by Def3;
hence H₂(x) in S ; :: thesis: verum

end;

end;

end;

consider h being Function of S,S such that
A7: for x being object st x in S holds
h . x = H₂(x) from FUNCT_2:sch 2(A5);
deffunc H₃( object ) -> Element of S = (h |** (k_nat $1)) . s0;
A8: for n being object st n in NAT holds
H₃(n) in S ;
consider pai being sequence of S such that
A9: for n being object st n in NAT holds
pai . n = H₃(n) from FUNCT_2:sch 2(A8);
A10: pai . 0 = H₃( 0 ) by A9
.= (h |** 0) . s0 by Def2
.= (id S) . s0 by FUNCT_7:84
.= s0 ;
A11: s0 in S ;
A12: for n being Nat holds
( [(pai . n),(pai . (n + 1))] in R & pai . (In (n,NAT)) |= g )

proof

defpred S₁[ Nat] means ( [(pai . $1),(pai . ($1 + 1))] in R & pai . (In ($1,NAT)) |= g );
A13: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
set k1 = k + 1;
set k2 = (k + 1) + 1;
set p0 = pai . (In (k,NAT));
set p1 = pai . (k + 1);
set p2 = pai . ((k + 1) + 1);
set Y1 = H₁(pai . (In (k,NAT))) /\ (SIGMA g);
set Y2 = H₁(pai . (k + 1)) /\ (SIGMA g);
A14: s0 in dom (h |** k) by A11, FUNCT_2:def 1;
assume S₁[k] ; :: thesis: S₁[k + 1]
then pai . (In (k,NAT)) |= EX g by A2;
then consider pai01 being inf_path of R such that
A15: pai01 . 0 = pai . (In (k,NAT)) and
A16: pai01 . 1 |= g by Th14;
set x1 = pai01 . 1;
[(pai01 . 0),(pai01 . (0 + 1))] in R by Def39;
then A17: pai01 . 1 in H₁(pai . (In (k,NAT))) by A15;
pai01 . 1 in SIGMA g by A16;
then H₁(pai . (In (k,NAT))) /\ (SIGMA g) <> {} by A17, XBOOLE_0:def 4;
then not H₁(pai . (In (k,NAT))) /\ (SIGMA g) in {{}} by TARSKI:def 1;
then A18: H₁(pai . (In (k,NAT))) /\ (SIGMA g) in (bool S) \ {{}} by XBOOLE_0:def 5;
then A19: H₁(pai . (In (k,NAT))) /\ (SIGMA g) in BOOL S by ORDERS_1:def 3;
A20: H₁(pai . (In (k,NAT))) /\ (SIGMA g) in dom Choice by A3, A18, ORDERS_1:def 3;
A21: k in NAT by ORDINAL1:def 12;
pai . (k + 1) = H₃(k + 1) by A9
.= (h |** (k + 1)) . s0 by Def2
.= (h * (h |** k)) . s0 by FUNCT_7:71
.= h . ((h |** k) . s0) by A14, FUNCT_1:13
.= h . H₃(k) by Def2, A21
.= h . (pai . (In (k,NAT))) by A9
.= H₂(pai . (In (k,NAT))) by A7
.= Choice . (H₁(pai . (In (k,NAT))) /\ (SIGMA g)) by A20, Def3 ;
then pai . (k + 1) in H₁(pai . (In (k,NAT))) /\ (SIGMA g) by A4, A19;
then pai . (k + 1) in SIGMA g by XBOOLE_0:def 4;
then A22: ex q1 being Element of S st
( q1 = pai . (k + 1) & q1 |= g ) ;
then pai . (k + 1) |= EX g by A2;
then consider pai02 being inf_path of R such that
A23: pai02 . 0 = pai . (k + 1) and
A24: pai02 . 1 |= g by Th14;
set x2 = pai02 . 1;
[(pai02 . 0),(pai02 . (0 + 1))] in R by Def39;
then A25: pai02 . 1 in H₁(pai . (k + 1)) by A23;
pai02 . 1 in SIGMA g by A24;
then pai02 . 1 in H₁(pai . (k + 1)) /\ (SIGMA g) by A25, XBOOLE_0:def 4;
then not H₁(pai . (k + 1)) /\ (SIGMA g) in {{}} by TARSKI:def 1;
then A26: H₁(pai . (k + 1)) /\ (SIGMA g) in (bool S) \ {{}} by XBOOLE_0:def 5;
then A27: H₁(pai . (k + 1)) /\ (SIGMA g) in BOOL S by ORDERS_1:def 3;
A28: s0 in dom (h |** (k + 1)) by A11, FUNCT_2:def 1;
A29: H₁(pai . (k + 1)) /\ (SIGMA g) in dom Choice by A3, A26, ORDERS_1:def 3;
pai . ((k + 1) + 1) = H₃((k + 1) + 1) by A9
.= (h |** ((k + 1) + 1)) . s0 by Def2
.= (h * (h |** (k + 1))) . s0 by FUNCT_7:71
.= h . ((h |** (k + 1)) . s0) by A28, FUNCT_1:13
.= h . H₃(k + 1) by Def2
.= h . (pai . (k + 1)) by A9
.= H₂(pai . (k + 1)) by A7
.= Choice . (H₁(pai . (k + 1)) /\ (SIGMA g)) by A29, Def3 ;
then pai . ((k + 1) + 1) in H₁(pai . (k + 1)) /\ (SIGMA g) by A4, A27;
then pai . ((k + 1) + 1) in H₁(pai . (k + 1)) by XBOOLE_0:def 4;
then ex q2 being Element of S st
( q2 = pai . ((k + 1) + 1) & [(pai . (k + 1)),q2] in R ) ;
hence S₁[k + 1] by A22; :: thesis: verum

end;

A30: S₁[ 0 ]

proof

set Y = H₁(s0) /\ (SIGMA g);
set y = Choice . (H₁(s0) /\ (SIGMA g));
s0 |= EX g by A1, A2;
then consider pai01 being inf_path of R such that
A31: pai01 . 0 = s0 and
A32: pai01 . 1 |= g by Th14;
set x = pai01 . 1;
[(pai01 . 0),(pai01 . (0 + 1))] in R by Def39;
then A33: pai01 . 1 in H₁(s0) by A31;
pai01 . 1 in SIGMA g by A32;
then H₁(s0) /\ (SIGMA g) <> {} by A33, XBOOLE_0:def 4;
then not H₁(s0) /\ (SIGMA g) in {{}} by TARSKI:def 1;
then A34: H₁(s0) /\ (SIGMA g) in (bool S) \ {{}} by XBOOLE_0:def 5;
then A35: H₁(s0) /\ (SIGMA g) in dom Choice by A3, ORDERS_1:def 3;
H₁(s0) /\ (SIGMA g) in BOOL S by A34, ORDERS_1:def 3;
then A36: Choice . (H₁(s0) /\ (SIGMA g)) in H₁(s0) /\ (SIGMA g) by A4;
then Choice . (H₁(s0) /\ (SIGMA g)) in H₁(s0) by XBOOLE_0:def 4;
then consider t being Element of S such that
A37: Choice . (H₁(s0) /\ (SIGMA g)) = t and
A38: [s0,t] in R ;
t in SIGMA g by A36, A37, XBOOLE_0:def 4;
then consider s1 being Element of S such that
A39: t = s1 and
s1 |= g ;
pai . 1 = H₃(1) by A9
.= (h |** 1) . s0 by Def2
.= h . s0 by FUNCT_7:70
.= H₂(s0) by A7
.= s1 by A35, A37, A39, Def3 ;
hence S₁[ 0 ] by A1, A10, A38, A39; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A30, A13);
hence for n being Nat holds
( [(pai . n),(pai . (n + 1))] in R & pai . (In (n,NAT)) |= g ) ; :: thesis: verum

end;

then reconsider pai = pai as inf_path of R by Def39;
take pai ; :: thesis: ( pai . 0 = s0 & ( for n being Nat holds pai . (In (n,NAT)) |= g ) )
thus ( pai . 0 = s0 & ( for n being Nat holds pai . (In (n,NAT)) |= g ) ) by A10, A12; :: thesis: verum