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