let P1, P2 be RelStr ; :: thesis: ( RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) & P1 is complete implies P2 is complete )
assume that
A1: RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) and
A2: for X being set ex a being Element of P1 st
( X is_<=_than a & ( for b being Element of P1 st X is_<=_than b holds
a <= b ) ) ; :: according to LATTICE3:def 12 :: thesis: P2 is complete
let X be set ; :: according to LATTICE3:def 12 :: thesis: ex b₁ being Element of the carrier of P2 st
( X is_<=_than b₁ & ( for b₂ being Element of the carrier of P2 holds
( not X is_<=_than b₂ or b₁ <= b₂ ) ) )
consider a being Element of P1 such that
A3: X is_<=_than a and
A4: for b being Element of P1 st X is_<=_than b holds
a <= b by A2;
reconsider a9 = a as Element of P2 by A1;
take a9 ; :: thesis: ( X is_<=_than a9 & ( for b₁ being Element of the carrier of P2 holds
( not X is_<=_than b₁ or a9 <= b₁ ) ) )
thus X is_<=_than a9 by A1, A3, Th2; :: thesis: for b₁ being Element of the carrier of P2 holds
( not X is_<=_than b₁ or a9 <= b₁ )
let b9 be Element of P2; :: thesis: ( not X is_<=_than b9 or a9 <= b9 )
reconsider b = b9 as Element of P1 by A1;
assume X is_<=_than b9 ; :: thesis: a9 <= b9
then a <= b by A1, A4, Th2;
hence a9 <= b9 by A1, Th1; :: thesis: verum