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