defpred S₁[ 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₁[x,y] holds
S₁[y,x] ;
A2: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by Th7;
A3: for x being object st x in Prop Q holds
S₁[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₁[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 )

proof

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 )

proof

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;

assume p <==> q ; :: thesis: [p,q] in R
hence [p,q] in R by A4; :: thesis: verum

end;

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