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