defpred S_{1}[ object , object ] means ex p, q being Element of Prop Q st

( p = $1 & q = $2 & p <==> q );

A1: for x, y being object st S_{1}[x,y] holds

S_{1}[y,x]
;

A2: for x, y, z being object st S_{1}[x,y] & S_{1}[y,z] holds

S_{1}[x,z]
by Th7;

A3: for x being object st x in Prop Q holds

S_{1}[x,x]
;

consider R being Equivalence_Relation of (Prop Q) such that

A4: for x, y being object holds

( [x,y] in R iff ( x in Prop Q & y in Prop Q & S_{1}[x,y] ) )
from EQREL_1:sch 1(A3, A1, A2);

take R ; :: thesis: for p, q being Element of Prop Q holds

( [p,q] in R iff p <==> q )

for p, q being Element of Prop Q holds

( [p,q] in R iff p <==> q )

( [p,q] in R iff p <==> q ) ; :: thesis: verum

( p = $1 & q = $2 & p <==> q );

A1: for x, y being object st S

S

A2: for x, y, z being object st S

S

A3: for x being object st x in Prop Q holds

S

consider R being Equivalence_Relation of (Prop Q) such that

A4: for x, y being object holds

( [x,y] in R iff ( x in Prop Q & y in Prop Q & S

take R ; :: thesis: for p, q being Element of Prop Q holds

( [p,q] in R iff p <==> q )

for p, q being Element of Prop Q holds

( [p,q] in R iff p <==> q )

proof

hence
for p, q being Element of Prop Q holds
let p, q be Element of Prop Q; :: thesis: ( [p,q] in R iff p <==> q )

thus ( [p,q] in R implies p <==> q ) :: thesis: ( p <==> q implies [p,q] in R )

hence [p,q] in R by A4; :: thesis: verum

end;thus ( [p,q] in R implies p <==> q ) :: thesis: ( p <==> q implies [p,q] in R )

proof

assume
p <==> q
; :: thesis: [p,q] in R
assume
[p,q] in R
; :: thesis: p <==> q

then ex p1, q1 being Element of Prop Q st

( p1 = p & q1 = q & p1 <==> q1 ) by A4;

hence p <==> q ; :: thesis: verum

end;then ex p1, q1 being Element of Prop Q st

( p1 = p & q1 = q & p1 <==> q1 ) by A4;

hence p <==> q ; :: thesis: verum

hence [p,q] in R by A4; :: thesis: verum

( [p,q] in R iff p <==> q ) ; :: thesis: verum