let T be non empty TopRelStr ; :: thesis:
assume T is anti-discrete ; :: thesis:
then reconsider W = T as non empty anti-discrete TopRelStr ;
set J = { the carrier of W};

end;

let x be Point of W; :: according to WAYBEL30:def 4 :: thesis:
reconsider J = { the carrier of W} as Basis of x by YELLOW13:13;
take J ; :: thesis:
let A be Subset of W; :: thesis:
assume A in J ; :: thesis:
hence subrelstr A is meet-inheriting by A5; :: thesis:

end;

let x be Point of W; :: according to WAYBEL30:def 2 :: thesis:
reconsider J = { the carrier of W} as basis of x by YELLOW13:21;
take J ; :: thesis:
let A be Subset of W; :: thesis:
assume A in J ; :: thesis:
hence subrelstr A is meet-inheriting by A5; :: thesis:

end;