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_{1} being Element of the carrier of T st

( b_{1} <= x & b_{1} <= y & ( for b_{2} being Element of the carrier of T holds

( not b_{2} <= x or not b_{2} <= y or b_{2} <= b_{1} ) ) )

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_{1} being Element of the carrier of T holds

( not b_{1} <= x or not b_{1} <= y or b_{1} <= z ) ) )

thus ( z <= x & z <= y ) by A1, A2, YELLOW_0:1; :: thesis: for b_{1} being Element of the carrier of T holds

( not b_{1} <= x or not b_{1} <= y or b_{1} <= 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

let x, y be Element of T; :: according to LATTICE3:def 11 :: thesis: ex b

( b

( not 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

( not b

thus ( z <= x & z <= y ) by A1, A2, YELLOW_0:1; :: thesis: for b

( not b

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