let A be Tolerance_Space; :: thesis: for X being Subset of
for x being set st x in UAp X holds
Class the InternalRel of A,x meets X
let X be Subset of ; :: thesis: for x being set st x in UAp X holds
Class the InternalRel of A,x meets X
let x be set ; :: thesis: ( x in UAp X implies Class the InternalRel of A,x meets X )
assume x in UAp X ; :: thesis: Class the InternalRel of A,x meets X
then ex x1 being Element of st
( x = x1 & Class the InternalRel of A,x1 meets X ) ;
hence Class the InternalRel of A,x meets X ; :: thesis: verum