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 T1, T2 being Subset of S st Tau T1,R,BASSIGN = Tau T2,R,BASSIGN holds
T1 = T2
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for T1, T2 being Subset of S st Tau T1,R,BASSIGN = Tau T2,R,BASSIGN holds
T1 = T2
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for T1, T2 being Subset of S st Tau T1,R,BASSIGN = Tau T2,R,BASSIGN holds
T1 = T2
let T1, T2 be Subset of S; :: thesis: ( Tau T1,R,BASSIGN = Tau T2,R,BASSIGN implies T1 = T2 )
set h1 = Tau T1,R,BASSIGN;
set h2 = Tau T2,R,BASSIGN;
assume A1: Tau T1,R,BASSIGN = Tau T2,R,BASSIGN ; :: thesis: T1 = T2
A2: for s being set st s in T1 holds
s in T2

proof

let s be set ; :: thesis: ( s in T1 implies s in T2 )
assume A3: s in T1 ; :: thesis: s in T2
then (chi T1,S) . s = 1 by FUNCT_3:def 3;
then (Fid (Tau T1,R,BASSIGN),S) . s = TRUE by A3, Def64;
then (chi T2,S) . s = 1 by A1, A3, Def64;
hence s in T2 by FUNCT_3:42; :: thesis: verum

end;

for s being set st s in T2 holds
s in T1

proof

let s be set ; :: thesis: ( s in T2 implies s in T1 )
assume A4: s in T2 ; :: thesis: s in T1
then (chi T2,S) . s = 1 by FUNCT_3:def 3;
then (Fid (Tau T2,R,BASSIGN),S) . s = TRUE by A4, Def64;
then (chi T1,S) . s = 1 by A1, A4, Def64;
hence s in T1 by FUNCT_3:42; :: thesis: verum

end;

hence T1 = T2 by A2, TARSKI:2; :: thesis: verum