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: 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 )
proof
let x be Element of L2; :: thesis: ( not compactbelow x is empty & compactbelow x is directed )
reconsider x9 = x as Element of L1 by A1;
( not compactbelow x9 is empty & compactbelow x9 is directed ) by A2;
hence ( not compactbelow x is empty & compactbelow x is directed ) by A1, A2, A3, Th10, WAYBEL_0:3; :: thesis: verum
end;
L2 is satisfying_axiom_K by A1, A2, A3, Th16;
hence L2 is algebraic by A3, A4; :: thesis: verum