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