let L1, L2 be non empty reflexive antisymmetric RelStr ; ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is algebraic implies L2 is algebraic )
assume that
A1:
RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #)
and
A2:
L1 is algebraic
; L2 is algebraic
A3:
L2 is up-complete
by A1, A2, Th15;
A4:
for x being Element of L2 holds
( not compactbelow x is empty & compactbelow x is directed )
L2 is satisfying_axiom_K
by A1, A2, A3, Th16;
hence
L2 is algebraic
by A3, A4; verum