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
A2: 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
A3: 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

A4: now

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 A2;
hence ( [B,C] in R1 iff [B,C] in R2 ) by A3; :: thesis: verum

end;

for x, y being set holds
( [x,y] in R1 iff [x,y] in R2 )

proof

let x, y be set ; :: 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 A5: [x,y] in R1 ; :: thesis: [x,y] in R2
then ( x in Class (PropRel Q) & y in Class (PropRel Q) ) by ZFMISC_1:106;
hence [x,y] in R2 by A4, A5; :: thesis: verum

end;

assume A6: [x,y] in R2 ; :: thesis: [x,y] in R1
then ( x in Class (PropRel Q) & y in Class (PropRel Q) ) by ZFMISC_1:106;
hence [x,y] in R1 by A4, A6; :: thesis: verum

end;

hence R1 = R2 by RELAT_1:def 2; :: thesis: verum