theorem Th27: :: WAYBEL14:27

for L being complete Scott TopLattice
for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X holds
( V is co-prime iff ( X is filtered & X is upper ) )