let R1, R2 be Relation of (Class (PropRel Q)); :: thesis: ( ( for B, C being Subset of (Prop Q) holds
( [B,C] in R1 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( 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 (PropRel Q) & C in Class (PropRel Q) & ( 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 (PropRel Q) & C in Class (PropRel Q) & ( 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 (PropRel Q) & C in Class (PropRel Q) & ( 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 (PropRel Q) & C in Class (PropRel Q) & ( 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 (PropRel Q) & y in Class (PropRel Q) ) 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 (PropRel Q) & y in Class (PropRel Q) ) 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