let R1, R2 be LATTICE; :: thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is complete implies R2 is complete )
assume that
A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) and
A2: R1 is complete ; :: thesis: R2 is complete
let X be set ; :: according to LATTICE3:def 12 :: thesis: ex b₁ being Element of the carrier of R2 st
( X is_<=_than b₁ & ( for b₂ being Element of the carrier of R2 holds
( not X is_<=_than b₂ or b₁ <= b₂ ) ) )
consider a1 being Element of R1 such that
A3: X is_<=_than a1 and
A4: for b being Element of R1 st X is_<=_than b holds
a1 <= b by A2;
reconsider a2 = a1 as Element of R2 by A1;
take a2 ; :: thesis: ( X is_<=_than a2 & ( for b₁ being Element of the carrier of R2 holds
( not X is_<=_than b₁ or a2 <= b₁ ) ) )
thus X is_<=_than a2 by A1, A3, Lm10; :: thesis: for b₁ being Element of the carrier of R2 holds
( not X is_<=_than b₁ or a2 <= b₁ )
let b2 be Element of R2; :: thesis: ( not X is_<=_than b2 or a2 <= b2 )
reconsider b1 = b2 as Element of R1 by A1;
assume X is_<=_than b2 ; :: thesis: a2 <= b2
then X is_<=_than b1 by A1, Lm10;
hence a2 <= b2 by A1, A4, Lm1; :: thesis: verum