let T be TopAugmentation of R; :: thesis: T is with_infima
let x, y be Element of T; :: according to LATTICE3:def 11 :: thesis: ex b₁ being Element of the carrier of T st
( b₁ <= x & b₁ <= y & ( for b₂ being Element of the carrier of T holds
( not b₂ <= x or not b₂ <= y or b₂ <= b₁ ) ) )
A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def 4;
then reconsider x9 = x, y9 = y as Element of R ;
consider z9 being Element of R such that
A2: ( z9 <= x9 & z9 <= y9 ) and
A3: for v9 being Element of R st v9 <= x9 & v9 <= y9 holds
v9 <= z9 by LATTICE3:def 11;
reconsider z = z9 as Element of T by A1;
take z ; :: thesis: ( z <= x & z <= y & ( for b₁ being Element of the carrier of T holds
( not b₁ <= x or not b₁ <= y or b₁ <= z ) ) )
thus ( z <= x & z <= y ) by A1, A2, YELLOW_0:1; :: thesis: for b₁ being Element of the carrier of T holds
( not b₁ <= x or not b₁ <= y or b₁ <= z )
let v be Element of T; :: thesis: ( not v <= x or not v <= y or v <= z )
reconsider v9 = v as Element of R by A1;
assume ( v <= x & v <= y ) ; :: thesis: v <= z
then ( v9 <= x9 & v9 <= y9 ) by A1, YELLOW_0:1;
then v9 <= z9 by A3;
hence v <= z by A1, YELLOW_0:1; :: thesis: verum