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_infima implies L2 is with_infima )
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 z9 being Element of L1 st z9 <= x & z9 <= y holds
z9 <= z ) ) ; :: according to LATTICE3:def 11 :: thesis: L2 is with_infima
let a, b be Element of L2; :: according to LATTICE3:def 11 :: thesis: ex b₁ being Element of the carrier of L2 st
( b₁ <= a & b₁ <= b & ( for b₂ being Element of the carrier of L2 holds
( not b₂ <= a 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 z9 being Element of L1 st z9 <= x & z9 <= y holds
z9 <= z by A2;
reconsider c = z as Element of L2 by A1;
take c ; :: thesis: ( c <= a & c <= b & ( for b₁ being Element of the carrier of L2 holds
( not b₁ <= a or not b₁ <= b or b₁ <= c ) ) )
thus ( c <= a & c <= b ) by A1, A3; :: thesis: for b₁ being Element of the carrier of L2 holds
( not b₁ <= a or not b₁ <= b or b₁ <= c )
let d be Element of L2; :: thesis: ( not d <= a or not d <= b or d <= c )
reconsider z9 = d as Element of L1 by A1;
assume ( d <= a & d <= b ) ; :: thesis: d <= c
then ( z9 <= x & z9 <= y ) by A1;
then z9 <= z by A4;
hence d <= c by A1; :: thesis: verum