let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ) implies L2 is satisfying_axiom_K )
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 satisfying_axiom_K and
A3: for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ; :: thesis: L2 is satisfying_axiom_K

now :: thesis: for x being Element of L2 holds x = sup (compactbelow x)

let x be Element of L2; :: thesis: x = sup (compactbelow x)
reconsider x9 = x as Element of L1 by A1;
( not compactbelow x9 is empty & compactbelow x9 is directed ) by A3;
then A4: ex_sup_of compactbelow x9,L1 by WAYBEL_0:75;
( x9 = sup (compactbelow x9) & compactbelow x = compactbelow x9 ) by A1, A2, Th10;
hence x = sup (compactbelow x) by A1, A4, YELLOW_0:26; :: thesis: verum

end;

hence L2 is satisfying_axiom_K ; :: thesis: verum