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

( [x,y] in R1 iff [x,y] 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 ) ) ) ) & ( 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 )

for x, y being object 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;( [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

( [x,y] in R1 iff [x,y] in R2 )

proof

hence
R1 = R2
by RELAT_1:def 2; :: thesis: verum
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 )

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;thus ( [x,y] in R1 implies [x,y] in R2 ) :: thesis: ( [x,y] in R2 implies [x,y] in R1 )

proof

assume A7:
[x,y] in R2
; :: thesis: [x,y] in R1
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;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

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