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 f, g, h being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) holds
for s being Element of S st s |= f EU g holds
s |= h
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) holds
for s being Element of S st s |= f EU g holds
s |= h
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g, h being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) holds
for s being Element of S st s |= f EU g holds
s |= h
let f, g, h be Assign of (BASSModel (R,BASSIGN)); :: thesis: ( ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) implies for s being Element of S st s |= f EU g holds
s |= h )
assume A1: for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ; :: thesis: for s being Element of S st s |= f EU g holds
s |= h
let s0 be Element of S; :: thesis: ( s0 |= f EU g implies s0 |= h )
assume s0 |= f EU g ; :: thesis: s0 |= h
then consider pai being inf_path of R such that
A2: pai . 0 = s0 and
A3: ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= f ) & pai . m |= g ) by Th16;
consider m being Element of NAT such that
A4: for j being Element of NAT st j < m holds
pai . j |= f and
A5: pai . m |= g by A3;
for j being Element of NAT st j <= m holds
pai . (k_nat (m - j)) |= h

proof

defpred S₁[ Nat] means ( $1 <= m implies pai . (k_nat (m - $1)) |= h );
A6: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A7: S₁[j] ; :: thesis: S₁[j + 1]
set j1 = j + 1;
( j + 1 <= m implies pai . (k_nat (m - (j + 1))) |= h )

proof

set k = m - (j + 1);
assume A8: j + 1 <= m ; :: thesis: pai . (k_nat (m - (j + 1))) |= h
then reconsider k = m - (j + 1) as Element of NAT by NAT_1:21;
set pai1 = PathShift (pai,k);
A9: (PathShift (pai,k)) . 0 = pai . (k + 0) by Def67
.= pai . k ;
k <= k + j by NAT_1:12;
then k < (k + j) + 1 by NAT_1:13;
then A10: pai . k |= f by A4;
A11: (PathShift (pai,k)) . 1 = pai . (k + 1) by Def67;
pai . (k + 1) |= h by A7, A8, Def2, NAT_1:13;
then pai . k |= EX h by A9, A11, Th14;
then pai . k |= Fax (f,h) by A10, Th13;
then A12: pai . k |= Foax (g,f,h) by Th17;
k_nat k = k by Def2;
hence pai . (k_nat (m - (j + 1))) |= h by A1, A12; :: thesis: verum

end;

hence S₁[j + 1] ; :: thesis: verum

end;

A13: S₁[ 0 ]

proof

assume 0 <= m ; :: thesis: pai . (k_nat (m - 0)) |= h
A14: k_nat (m - 0) = m by Def2;
pai . m |= Foax (g,f,h) by A5, Th17;
hence pai . (k_nat (m - 0)) |= h by A1, A14; :: thesis: verum

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A13, A6);
hence for j being Element of NAT st j <= m holds
pai . (k_nat (m - j)) |= h ; :: thesis: verum

end;

then pai . (k_nat (m - m)) |= h ;
hence s0 |= h by A2, Def2; :: thesis: verum