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:
proof
let a be Element of L; :: according to YELLOW_4:def 1 :: thesis: ( not a in A or ex b1 being Element of the carrier of L st
( b1 in B & a <= b1 ) )

assume A2: a in A ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in B & a <= b1 )

take b = a; :: thesis: ( b in B & a <= b )
thus ( b in B & a <= b ) by A1, A2; :: thesis: verum
end;
let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in A or ex b1 being Element of the carrier of L st
( b1 in B & b1 <= a ) )

assume A3: a in A ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in B & b1 <= a )

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