let L be RelStr ; :: thesis: for A being Subset of holds {} L is_coarser_than A
let A be Subset of ; :: thesis: {} L is_coarser_than A
let b be Element of ; :: according to YELLOW_4:def 2 :: thesis: ( b in {} L implies ex a being Element of st
( a in A & a <= b ) )
assume b in {} L ; :: thesis: ex a being Element of st
( a in A & a <= b )
hence ex a being Element of st
( a in A & a <= b ) ; :: thesis: verum