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 x' = x, y' = y as Element of R ;
consider z' being Element of R such that
A2: ( z' <= x' & z' <= y' ) and
A3: for v' being Element of R st v' <= x' & v' <= y' holds
v' <= z' by LATTICE3:def 11;
reconsider z = z' 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 v' = v as Element of R by A1;
assume ( v <= x & v <= y ) ; :: thesis: v <= z
then ( v' <= x' & v' <= y' ) by A1, YELLOW_0:1;
then v' <= z' by A3;
hence v <= z by A1, YELLOW_0:1; :: thesis: verum