let A be Tolerance_Space; :: thesis: for X being Subset of A
for x being set st x in UAp X holds
Class the InternalRel of A,x meets X
let X be Subset of A; :: 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 consider x1 being Element of A such that
A1: ( x = x1 & Class the InternalRel of A,x1 meets X ) ;
thus Class the InternalRel of A,x meets X by A1; :: thesis: verum