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₁ being Element of the carrier of T st
( b₁ is_<=_than X & ( for b₂ being Element of the carrier of T holds
( not b₂ is_<=_than X 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 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₁ being Element of the carrier of T holds
( not b₁ is_<=_than X or b₁ <= y ) ) )
thus y is_<=_than X by A1, A2, YELLOW_0:2; :: thesis: for b₁ being Element of the carrier of T holds
( not b₁ is_<=_than X or b₁ <= 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