let L1, L2 be non empty reflexive antisymmetric RelStr ; :: thesis: ( 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 ; :: thesis: L2 is algebraic
A3: ( ( for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ) & L1 is up-complete & L1 is satisfying_axiom_K ) by A2, Def4;
then A4: L2 is up-complete by A1, Th15;
A5: for x being Element of L2 holds
( not compactbelow x is empty & compactbelow x is directed )

proof

let x be Element of L2; :: thesis: ( not compactbelow x is empty & compactbelow x is directed )
reconsider x' = x as Element of L1 by A1;
A6: ( not compactbelow x' is empty & compactbelow x' is directed ) by A2, Def4;
compactbelow x' = compactbelow x by A1, A3, A4, Th10;
hence ( not compactbelow x is empty & compactbelow x is directed ) by A1, A6, WAYBEL_0:3; :: thesis: verum

end;

L2 is satisfying_axiom_K by A1, A3, A4, Th16;
hence L2 is algebraic by A4, A5, Def4; :: thesis: verum