let S be non empty set ; :: thesis: for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= EX f iff ex s1 being Element of S st
( [s,s1] in R & s1 |= f ) )
let R be total Relation of S,S; :: thesis: for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= EX f iff ex s1 being Element of S st
( [s,s1] in R & s1 |= f ) )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= EX f iff ex s1 being Element of S st
( [s,s1] in R & s1 |= f ) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= EX f iff ex s1 being Element of S st
( [s,s1] in R & s1 |= f ) )
let f be Assign of (BASSModel (R,BASSIGN)); :: thesis: ( s |= EX f iff ex s1 being Element of S st
( [s,s1] in R & s1 |= f ) )
A1: ( s |= EX f implies ex s1 being Element of S st
( [s,s1] in R & s1 |= f ) )

proof

assume s |= EX f ; :: thesis: ex s1 being Element of S st
( [s,s1] in R & s1 |= f )
then consider pai being inf_path of R such that
A2: pai . 0 = s and
A3: pai . 1 |= f by Th14;
[(pai . 0),(pai . (0 + 1))] in R by Def39;
hence ex s1 being Element of S st
( [s,s1] in R & s1 |= f ) by A2, A3; :: thesis: verum

end;

( ex s1 being Element of S st
( [s,s1] in R & s1 |= f ) implies s |= EX f )

proof

given s1 being Element of S such that A4: [s,s1] in R and
A5: s1 |= f ; :: thesis: s |= EX f
ex pai being inf_path of R st
( pai . 0 = s & pai . 1 = s1 ) by A4, Th27;
hence s |= EX f by A5, Th14; :: thesis: verum

end;

hence ( s |= EX f iff ex s1 being Element of S st
( [s,s1] in R & s1 |= f ) ) by A1; :: thesis: verum