let R be Relation; :: thesis: fixpoints1 R = fixpoints1 (R ~)
set Q = R ~ ;
set dq = dom (R ~);
set dr = dom R;
set rq = rng (R ~);
set rr = rng R;
set iq = id ((dom (R ~)) /\ (rng (R ~)));
set ir = id ((dom R) /\ (rng R));
set r = R /\ (id ((dom R) /\ (rng R)));
set q = (R ~) /\ (id ((dom (R ~)) /\ (rng (R ~))));
reconsider r = R /\ (id ((dom R) /\ (rng R))) as Subset of (id ((dom R) /\ (rng R))) ;
( dom (R ~) = rng R & rng (R ~) = dom R ) by RELAT_1:20;
then (R ~) /\ (id ((dom (R ~)) /\ (rng (R ~)))) = (R ~) /\ ((id ((dom R) /\ (rng R))) ~)
.= r ~ by RELAT_1:22
.= r ;
hence fixpoints1 R = fixpoints1 (R ~) ; :: thesis: verum