let R1, R2 be Relation of (Class ()); :: thesis: ( ( for B, C being Subset of (Prop Q) holds
( [B,C] in R1 iff ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ) & ( for B, C being Subset of (Prop Q) holds
( [B,C] in R2 iff ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ) implies R1 = R2 )

assume that
A3: for B, C being Subset of (Prop Q) holds
( [B,C] in R1 iff ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) and
A4: for B, C being Subset of (Prop Q) holds
( [B,C] in R2 iff ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ; :: thesis: R1 = R2
A5: now :: thesis: for B, C being Subset of (Prop Q) holds
( [B,C] in R1 iff [B,C] in R2 )
let B, C be Subset of (Prop Q); :: thesis: ( [B,C] in R1 iff [B,C] in R2 )
( [B,C] in R1 iff ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) by A3;
hence ( [B,C] in R1 iff [B,C] in R2 ) by A4; :: thesis: verum
end;
for x, y being object holds
( [x,y] in R1 iff [x,y] in R2 )
proof
let x, y be object ; :: thesis: ( [x,y] in R1 iff [x,y] in R2 )
thus ( [x,y] in R1 implies [x,y] in R2 ) :: thesis: ( [x,y] in R2 implies [x,y] in R1 )
proof
assume A6: [x,y] in R1 ; :: thesis: [x,y] in R2
then ( x in Class () & y in Class () ) by ZFMISC_1:87;
hence [x,y] in R2 by A5, A6; :: thesis: verum
end;
assume A7: [x,y] in R2 ; :: thesis: [x,y] in R1
then ( x in Class () & y in Class () ) by ZFMISC_1:87;
hence [x,y] in R1 by A5, A7; :: thesis: verum
end;
hence R1 = R2 by RELAT_1:def 2; :: thesis: verum