let Q1, Q2 be invariant stable ManySortedRelation of A; :: thesis: ( R c= Q1 & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
Q1 c= Q ) & R c= Q2 & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
Q2 c= Q ) implies Q1 = Q2 )
assume that
A1: R c= Q1 and
A2: for Q being invariant stable ManySortedRelation of A st R c= Q holds
Q1 c= Q and
A3: R c= Q2 and
A4: for Q being invariant stable ManySortedRelation of A st R c= Q holds
Q2 c= Q ; :: thesis: Q1 = Q2
( Q1 c= Q2 & Q2 c= Q1 ) by A1, A2, A3, A4;
hence Q1 = Q2 by PBOOLE:146; :: thesis: verum