let L1, L2 be RelStr ; :: thesis: ( RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is with_suprema implies L2 is with_suprema )
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, y being Element of L1 ex z being Element of L1 st
( z >= x & z >= y & ( for z' being Element of L1 st z' >= x & z' >= y holds
z' >= z ) ) ; :: according to LATTICE3:def 10 :: thesis: L2 is with_suprema
let a, b be Element of L2; :: according to LATTICE3:def 10 :: thesis: ex b₁ being Element of the carrier of L2 st
( a <= b₁ & b <= b₁ & ( for b₂ being Element of the carrier of L2 holds
( not a <= b₂ or not b <= b₂ or b₁ <= b₂ ) ) )
reconsider x = a, y = b as Element of L1 by A1;
consider z being Element of L1 such that
A3: ( z >= x & z >= y ) and
A4: for z' being Element of L1 st z' >= x & z' >= y holds
z' >= z by A2;
reconsider c = z as Element of L2 by A1;
take c ; :: thesis: ( a <= c & b <= c & ( for b₁ being Element of the carrier of L2 holds
( not a <= b₁ or not b <= b₁ or c <= b₁ ) ) )
thus ( c >= a & c >= b ) by A1, A3, YELLOW_0:1; :: thesis: for b₁ being Element of the carrier of L2 holds
( not a <= b₁ or not b <= b₁ or c <= b₁ )
let d be Element of L2; :: thesis: ( not a <= d or not b <= d or c <= d )
reconsider z' = d as Element of L1 by A1;
assume ( d >= a & d >= b ) ; :: thesis: c <= d
then ( z' >= x & z' >= y ) by A1, YELLOW_0:1;
then z' >= z by A4;
hence c <= d by A1, YELLOW_0:1; :: thesis: verum