let L1 be non empty reflexive antisymmetric continuous RelStr ; :: thesis: for L2 being non empty reflexive RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) holds
L2 is continuous
let L2 be non empty reflexive RelStr ; :: thesis: ( RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) implies L2 is continuous )
assume A1: RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) ; :: thesis: L2 is continuous

hereby :: according to WAYBEL_3:def 6 :: thesis: ( L2 is up-complete & L2 is satisfying_axiom_of_approximation )

let y be Element of L2; :: thesis: ( not waybelow y is empty & waybelow y is directed )
reconsider x = y as Element of L1 by A1;
waybelow x = waybelow y by A1, Th13;
hence ( not waybelow y is empty & waybelow y is directed ) by A1, WAYBEL_0:3; :: thesis: verum

end;

thus L2 is up-complete by A1, WAYBEL_8:15; :: thesis: L2 is satisfying_axiom_of_approximation
let y be Element of L2; :: according to WAYBEL_3:def 5 :: thesis: y = "\/" (waybelow y),L2
reconsider x = y as Element of L1 by A1;
A2: ex_sup_of waybelow x,L1 by WAYBEL_0:75;
A3: waybelow x = waybelow y by A1, Th13;
x = sup (waybelow x) by WAYBEL_3:def 5;
hence y = "\/" (waybelow y),L2 by A1, A2, A3, YELLOW_0:26; :: thesis: verum