reconsider Q = InvCl (StabCl R) as invariant stable ManySortedRelation of A by Th30;
take Q ; :: thesis: ( R c= Q & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
Q c= Q ) )
A5: StabCl R c= InvCl (StabCl R) by Def11;
R c= StabCl R by Def12;
hence R c= Q by A5, PBOOLE:13; :: thesis: for Q being invariant stable ManySortedRelation of A st R c= Q holds
Q c= Q
let P be invariant stable ManySortedRelation of A; :: thesis: ( R c= P implies Q c= P )
assume R c= P ; :: thesis: Q c= P
then StabCl R c= P by Def12;
hence Q c= P by Def11; :: thesis: verum