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 a being Assign of (BASSModel (R,BASSIGN)) st a in BASSIGN holds
( s |= a iff a in (Label_ BASSIGN) . s )
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 a being Assign of (BASSModel (R,BASSIGN)) st a in BASSIGN holds
( s |= a iff a in (Label_ BASSIGN) . s )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for a being Assign of (BASSModel (R,BASSIGN)) st a in BASSIGN holds
( s |= a iff a in (Label_ BASSIGN) . s )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for a being Assign of (BASSModel (R,BASSIGN)) st a in BASSIGN holds
( s |= a iff a in (Label_ BASSIGN) . s )
let a be Assign of (BASSModel (R,BASSIGN)); :: thesis: ( a in BASSIGN implies ( s |= a iff a in (Label_ BASSIGN) . s ) )
assume A1: a in BASSIGN ; :: thesis: ( s |= a iff a in (Label_ BASSIGN) . s )
thus ( s |= a implies a in (Label_ BASSIGN) . s ) :: thesis: ( a in (Label_ BASSIGN) . s implies s |= a )

proof

set f = Fid (a,S);
assume s |= a ; :: thesis: a in (Label_ BASSIGN) . s
then A2: (Fid (a,S)) . s = TRUE ;
a = Fid (a,S) by Def41;
then a in F_LABEL (s,BASSIGN) by A1, A2, Def55;
hence a in (Label_ BASSIGN) . s by Def56; :: thesis: verum

end;

assume a in (Label_ BASSIGN) . s ; :: thesis: s |= a
then a in F_LABEL (s,BASSIGN) by Def56;
then consider f being Function of S,BOOLEAN such that
A3: f = a and
A4: f . s = TRUE by Def55;
Fid (a,S) = f by A3, Def41;
hence s |= a by A4; :: thesis: verum