let T be TopAugmentation of R; :: thesis: T is /\-complete

let X be non empty Subset of T; :: according to WAYBEL_0:def 40 :: thesis: ex b_{1} being Element of the carrier of T st

( b_{1} is_<=_than X & ( for b_{2} being Element of the carrier of T holds

( not b_{2} is_<=_than X 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 Y = X as non empty Subset of R ;

consider x being Element of R such that

A2: x is_<=_than Y and

A3: for y being Element of R st y is_<=_than Y holds

x >= y by WAYBEL_0:def 40;

reconsider y = x as Element of T by A1;

take y ; :: thesis: ( y is_<=_than X & ( for b_{1} being Element of the carrier of T holds

( not b_{1} is_<=_than X or b_{1} <= y ) ) )

thus y is_<=_than X by A1, A2, YELLOW_0:2; :: thesis: for b_{1} being Element of the carrier of T holds

( not b_{1} is_<=_than X or b_{1} <= y )

let z be Element of T; :: thesis: ( not z is_<=_than X or z <= y )

reconsider v = z as Element of R by A1;

assume z is_<=_than X ; :: thesis: z <= y

then x >= v by A1, A3, YELLOW_0:2;

hence z <= y by A1, YELLOW_0:1; :: thesis: verum

let X be non empty Subset of T; :: according to WAYBEL_0:def 40 :: 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 Y = X as non empty Subset of R ;

consider x being Element of R such that

A2: x is_<=_than Y and

A3: for y being Element of R st y is_<=_than Y holds

x >= y by WAYBEL_0:def 40;

reconsider y = x as Element of T by A1;

take y ; :: thesis: ( y is_<=_than X & ( for b

( not b

thus y is_<=_than X by A1, A2, YELLOW_0:2; :: thesis: for b

( not b

let z be Element of T; :: thesis: ( not z is_<=_than X or z <= y )

reconsider v = z as Element of R by A1;

assume z is_<=_than X ; :: thesis: z <= y

then x >= v by A1, A3, YELLOW_0:2;

hence z <= y by A1, YELLOW_0:1; :: thesis: verum