let X be StackAlgebra; :: thesis: for s1, s2 being stack of X ex s being stack of X st (coset s1) /\ (Class ((==_ X),s2)) = {s}
let s1, s2 be stack of X; :: thesis: ex s being stack of X st (coset s1) /\ (Class ((==_ X),s2)) = {s}
consider s being stack of X such that
A1: ( |.s.| = |.s2.| & s in coset s1 ) by Th30;
take s ; :: thesis: (coset s1) /\ (Class ((==_ X),s2)) = {s}
thus (coset s1) /\ (Class ((==_ X),s2)) c= {s} :: according to XBOOLE_0:def 10 :: thesis: {s} c= (coset s1) /\ (Class ((==_ X),s2))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (coset s1) /\ (Class ((==_ X),s2)) or x in {s} )
assume A2: x in (coset s1) /\ (Class ((==_ X),s2)) ; :: thesis: x in {s}
then A3: ( x in coset s1 & x in Class ((==_ X),s2) ) by XBOOLE_0:def 4;
reconsider x = x as stack of X by A2;
[s2,x] in ==_ X by A3, EQREL_1:18;
then s2 == x by Def16;
then |.s2.| = |.x.| ;
then s = x by A1, A3, Th32;
hence x in {s} by TARSKI:def 1; :: thesis: verum
end;
s == s2 by A1;
then [s2,s] in ==_ X by Def16;
then s in Class ((==_ X),s2) by EQREL_1:18;
then ( {s} c= Class ((==_ X),s2) & {s} c= coset s1 ) by A1, ZFMISC_1:31;
hence {s} c= (coset s1) /\ (Class ((==_ X),s2)) by XBOOLE_1:19; :: thesis: verum