let x be set ; :: thesis: for L being non empty reflexive transitive RelStr
for I being Element of st x in I holds
x is Element of
let L be non empty reflexive transitive RelStr ; :: thesis: for I being Element of st x in I holds
x is Element of
let I be Element of ; :: thesis: ( x in I implies x is Element of )
reconsider I' = I as non empty Subset of by Th43;
assume x in I ; :: thesis: x is Element of
then reconsider x' = x as Element of I' ;
x' in the carrier of L ;
hence x is Element of ; :: thesis: verum