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