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 #) & ( 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) ; :: according to WAYBEL_3:def 5 :: thesis: L2 is satisfying_axiom_of_approximation
let x be Element of L2; :: according to WAYBEL_3:def 5 :: thesis: 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; :: thesis: verum