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