thus for D1, D2 being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in D1 iff S₁[x,y] ) ) & ( for x, y being Element of A holds
( [x,y] in D2 iff S₁[x,y] ) ) holds
D1 = D2 from PUA2MSS1:sch 2(); :: thesis: verum