let L be non empty reflexive RelStr ; :: thesis: for A, B being Subset of L st A c= B holds

( A is_finer_than B & A is_coarser_than B )

let A, B be Subset of L; :: thesis: ( A c= B implies ( A is_finer_than B & A is_coarser_than B ) )

assume A1: A c= B ; :: thesis: ( A is_finer_than B & A is_coarser_than B )

thus A is_finer_than B :: thesis: A is_coarser_than B_{1} being Element of the carrier of L st

( b_{1} in B & b_{1} <= a ) )

assume A3: a in A ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in B & b_{1} <= a )

take b = a; :: thesis: ( b in B & b <= a )

thus ( b in B & b <= a ) by A1, A3; :: thesis: verum

( A is_finer_than B & A is_coarser_than B )

let A, B be Subset of L; :: thesis: ( A c= B implies ( A is_finer_than B & A is_coarser_than B ) )

assume A1: A c= B ; :: thesis: ( A is_finer_than B & A is_coarser_than B )

thus A is_finer_than B :: thesis: A is_coarser_than B

proof

let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in A or ex b
let a be Element of L; :: according to YELLOW_4:def 1 :: thesis: ( not a in A or ex b_{1} being Element of the carrier of L st

( b_{1} in B & a <= b_{1} ) )

assume A2: a in A ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in B & a <= b_{1} )

take b = a; :: thesis: ( b in B & a <= b )

thus ( b in B & a <= b ) by A1, A2; :: thesis: verum

end;( b

assume A2: a in A ; :: thesis: ex b

( b

take b = a; :: thesis: ( b in B & a <= b )

thus ( b in B & a <= b ) by A1, A2; :: thesis: verum

( b

assume A3: a in A ; :: thesis: ex b

( b

take b = a; :: thesis: ( b in B & b <= a )

thus ( b in B & b <= a ) by A1, A3; :: thesis: verum