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 b1 being Element of the carrier of T st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of T holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )

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 b1 being Element of the carrier of T holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )

thus ( z <= x & z <= y ) by ; :: thesis: for b1 being Element of the carrier of T holds
( not b1 <= x or not b1 <= y or b1 <= 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 ;
then v9 <= z9 by A3;
hence v <= z by ; :: thesis: verum