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 Element of NAT holds pai . n |= 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 Element of NAT holds pai . n |= 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 Element of NAT holds pai . n |= 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 Element of NAT holds pai . n |= 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 Element of NAT holds pai . n |= 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 Element of NAT holds pai . n |= g ) ) )
deffunc H₁( set ) -> 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 Element of NAT holds pai . n |= 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₂( set ) -> set = UnivF ((H₁($1) /\ (SIGMA g)),Choice,s0);
A5: for x being set st x in S holds
H₂(x) in S

proof

let x be set ; :: 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 set st x in S holds
h . x = H₂(x) from FUNCT_2:sch 2(A5);
deffunc H₃( set ) -> Element of S = (h |** (k_nat $1)) . s0;
A8: for n being set st n in NAT holds
H₃(n) in S ;
consider pai being Function of NAT,S such that
A9: for n being set 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 by FUNCT_1:18 ;
A11: s0 in S ;
A12: for n being Element of NAT holds
( [(pai . n),(pai . (n + 1))] in R & pai . n |= g )

proof

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

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
set k1 = k + 1;
set k2 = (k + 1) + 1;
set p0 = pai . k;
set p1 = pai . (k + 1);
set p2 = pai . ((k + 1) + 1);
set Y1 = H₁(pai . k) /\ (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 . k |= EX g by A2;
then consider pai01 being inf_path of R such that
A15: pai01 . 0 = pai . k and
A16: pai01 . 1 |= g by Th14;
set x1 = pai01 . 1;
[(pai01 . 0),(pai01 . (0 + 1))] in R by Def41;
then A17: pai01 . 1 in H₁(pai . k) by A15;
pai01 . 1 in SIGMA g by A16;
then H₁(pai . k) /\ (SIGMA g) <> {} by A17, XBOOLE_0:def 4;
then not H₁(pai . k) /\ (SIGMA g) in {{}} by TARSKI:def 1;
then A18: H₁(pai . k) /\ (SIGMA g) in (bool S) \ {{}} by XBOOLE_0:def 5;
then A19: H₁(pai . k) /\ (SIGMA g) in BOOL S by ORDERS_1:def 2;
A20: H₁(pai . k) /\ (SIGMA g) in dom Choice by A3, A18, ORDERS_1:def 2;
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
.= h . (pai . k) by A9
.= H₂(pai . k) by A7
.= Choice . (H₁(pai . k) /\ (SIGMA g)) by A20, Def3 ;
then pai . (k + 1) in H₁(pai . k) /\ (SIGMA g) by A4, A19;
then pai . (k + 1) in SIGMA g by XBOOLE_0:def 4;
then A21: 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
A22: pai02 . 0 = pai . (k + 1) and
A23: pai02 . 1 |= g by Th14;
set x2 = pai02 . 1;
[(pai02 . 0),(pai02 . (0 + 1))] in R by Def41;
then A24: pai02 . 1 in H₁(pai . (k + 1)) by A22;
pai02 . 1 in SIGMA g by A23;
then pai02 . 1 in H₁(pai . (k + 1)) /\ (SIGMA g) by A24, XBOOLE_0:def 4;
then not H₁(pai . (k + 1)) /\ (SIGMA g) in {{}} by TARSKI:def 1;
then A25: H₁(pai . (k + 1)) /\ (SIGMA g) in (bool S) \ {{}} by XBOOLE_0:def 5;
then A26: H₁(pai . (k + 1)) /\ (SIGMA g) in BOOL S by ORDERS_1:def 2;
A27: s0 in dom (h |** (k + 1)) by A11, FUNCT_2:def 1;
A28: H₁(pai . (k + 1)) /\ (SIGMA g) in dom Choice by A3, A25, ORDERS_1:def 2;
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 A27, 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 A28, Def3 ;
then pai . ((k + 1) + 1) in H₁(pai . (k + 1)) /\ (SIGMA g) by A4, A26;
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 A21; :: thesis: verum

end;

A29: 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
A30: pai01 . 0 = s0 and
A31: pai01 . 1 |= g by Th14;
set x = pai01 . 1;
[(pai01 . 0),(pai01 . (0 + 1))] in R by Def41;
then A32: pai01 . 1 in H₁(s0) by A30;
pai01 . 1 in SIGMA g by A31;
then H₁(s0) /\ (SIGMA g) <> {} by A32, XBOOLE_0:def 4;
then not H₁(s0) /\ (SIGMA g) in {{}} by TARSKI:def 1;
then A33: H₁(s0) /\ (SIGMA g) in (bool S) \ {{}} by XBOOLE_0:def 5;
then A34: H₁(s0) /\ (SIGMA g) in dom Choice by A3, ORDERS_1:def 2;
H₁(s0) /\ (SIGMA g) in BOOL S by A33, ORDERS_1:def 2;
then A35: 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
A36: Choice . (H₁(s0) /\ (SIGMA g)) = t and
A37: [s0,t] in R ;
t in SIGMA g by A35, A36, XBOOLE_0:def 4;
then consider s1 being Element of S such that
A38: 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 A34, A36, A38, Def3 ;
hence S₁[ 0 ] by A1, A10, A37, A38; :: thesis: verum

end;

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

end;

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