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 I' = I as non empty Subset of L by Th43;
assume x in I ; :: thesis: x is Element of L
then reconsider x' = x as Element of I' ;
x' in the carrier of L ;
hence x is Element of L ; :: thesis: verum