let L be non empty antisymmetric upper-bounded RelStr ; :: thesis: Top L is prime
let x, y be Element of L; :: according to WAYBEL_6:def 6 :: thesis: ( not x "/\" y <= Top L or x <= Top L or y <= Top L )
assume x "/\" y <= Top L ; :: thesis: ( x <= Top L or y <= Top L )
thus ( x <= Top L or y <= Top L ) by YELLOW_0:45; :: thesis: verum