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, h1, h2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= h1 holds
s |= h2 ) holds
for s being Element of S st s |= Foax (g,f,h1) holds
s |= Foax (g,f,h2)
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h1, h2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= h1 holds
s |= h2 ) holds
for s being Element of S st s |= Foax (g,f,h1) holds
s |= Foax (g,f,h2)
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g, h1, h2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= h1 holds
s |= h2 ) holds
for s being Element of S st s |= Foax (g,f,h1) holds
s |= Foax (g,f,h2)
let f, g, h1, h2 be Assign of (BASSModel (R,BASSIGN)); :: thesis: ( ( for s being Element of S st s |= h1 holds
s |= h2 ) implies for s being Element of S st s |= Foax (g,f,h1) holds
s |= Foax (g,f,h2) )
assume A1: for s being Element of S st s |= h1 holds
s |= h2 ; :: thesis: for s being Element of S st s |= Foax (g,f,h1) holds
s |= Foax (g,f,h2)
let s be Element of S; :: thesis: ( s |= Foax (g,f,h1) implies s |= Foax (g,f,h2) )
assume A2: s |= Foax (g,f,h1) ; :: thesis: s |= Foax (g,f,h2)
per cases ( s |= g or s |= Fax (f,h1) ) by A2, Th17;
suppose s |= g ; :: thesis: s |= Foax (g,f,h2)
hence s |= Foax (g,f,h2) by Th17; :: thesis: verum
end;
suppose A3: s |= Fax (f,h1) ; :: thesis: s |= Foax (g,f,h2)
then s |= EX h1 by Th13;
then consider pai being inf_path of R such that
A4: pai . 0 = s and
A5: pai . 1 |= h1 by Th14;
pai . 1 |= h2 by A1, A5;
then A6: s |= EX h2 by A4, Th14;
s |= f by A3, Th13;
then s |= f '&' (EX h2) by A6, Th13;
hence s |= Foax (g,f,h2) by Th17; :: thesis: verum
end;
end;