let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & ( for x being Element of L1 holds
( waybelow x is directed & not waybelow x is empty ) ) & L1 is satisfying_axiom_of_approximation implies L2 is satisfying_axiom_of_approximation )
assume that
A1:
RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #)
and
A2:
for x being Element of L1 holds
( waybelow x is directed & not waybelow x is empty )
and
A3:
for x being Element of L1 holds x = sup (waybelow x)
; WAYBEL_3:def 5 L2 is satisfying_axiom_of_approximation
let x be Element of L2; WAYBEL_3:def 5 x = "\/" ((waybelow x),L2)
reconsider y = x as Element of L1 by A1;
A4:
y = sup (waybelow y)
by A3;
( waybelow y is directed & not waybelow y is empty )
by A2;
then A5:
ex_sup_of waybelow y,L1
by WAYBEL_0:75;
waybelow y = waybelow x
by A1, YELLOW12:13;
hence
x = "\/" ((waybelow x),L2)
by A4, A5, A1, YELLOW_0:26; verum