let R1, R2 be complete LATTICE; :: thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is continuous implies R2 is continuous )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; :: thesis: ( not R1 is continuous or R2 is continuous )
assume A2: R1 is continuous ; :: thesis: R2 is continuous
thus A3: for x being Element of R2 holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def 6 :: thesis: ( R2 is up-complete & R2 is satisfying_axiom_of_approximation )
thus R2 is up-complete ; :: thesis: R2 is satisfying_axiom_of_approximation
for x, y being Element of R2 st not x <= y holds
ex u being Element of R2 st
( u << x & not u <= y )
proof
let x2, y2 be Element of R2; :: thesis: ( not x2 <= y2 implies ex u being Element of R2 st
( u << x2 & not u <= y2 ) )
reconsider x1 = x2, y1 = y2 as Element of R1 by A1;
assume not x2 <= y2 ; :: thesis: ex u being Element of R2 st
( u << x2 & not u <= y2 )
then not x1 <= y1 by A1, Lm1;
then consider u1 being Element of R1 such that
A4: u1 << x1 and
A5: not u1 <= y1 by A2, WAYBEL_3:24;
reconsider u2 = u1 as Element of R2 by A1;
take u2 ; :: thesis: ( u2 << x2 & not u2 <= y2 )
thus u2 << x2 by A1, A4, Lm15; :: thesis: not u2 <= y2
thus not u2 <= y2 by A1, A5, Lm1; :: thesis: verum
end;
hence R2 is satisfying_axiom_of_approximation by A3, WAYBEL_3:24; :: thesis: verum