let S be non empty set ; :: thesis:
let R be total Relation of S,S; :: thesis:
let BASSIGN be non empty Subset of (ModelSP S); :: thesis:
let T1, T2 be Subset of S; :: thesis:
set h1 = Tau (T1,R,BASSIGN);
set h2 = Tau (T2,R,BASSIGN);
assume A1: Tau (T1,R,BASSIGN) = Tau (T2,R,BASSIGN) ; :: thesis:
A2: for s being object st s in T2 holds
s in T1

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

end;

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

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

end;