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

thus y is_<=_than X by ; :: thesis: for b1 being Element of the carrier of T holds
( not b1 is_<=_than X or b1 <= 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 ;
hence z <= y by ; :: thesis: verum