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