let U1, U2 be Universal_Algebra; ( U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 implies U1 = U2 )
assume that
A1:
U1 is strict SubAlgebra of U2
and
A2:
U2 is strict SubAlgebra of U1
; U1 = U2
reconsider B = the carrier of U1 as non empty Subset of U2 by A1, Def7;
the carrier of U2 c= the carrier of U2
;
then reconsider B1 = the carrier of U2 as non empty Subset of U2 ;
A3:
dom (Opers (U2,B1)) = dom the charact of U2
by Def6;
A4:
for n being Nat st n in dom the charact of U2 holds
the charact of U2 . n = (Opers (U2,B1)) . n
the carrier of U2 is Subset of U1
by A2, Def7;
then A6:
B1 = B
;
then
the charact of U1 = Opers (U2,B1)
by A1, Def7;
hence
U1 = U2
by A1, A2, A6, A3, A4, FINSEQ_1:13; verum