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

proof

let a be Element of L; :: according to YELLOW_4:def 1 :: thesis: ( not a in A or ex b₁ being Element of the carrier of L st
( b₁ in B & a <= b₁ ) )
assume A2: a in A ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in B & a <= b₁ )
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 b₁ being Element of the carrier of L st
( b₁ in B & b₁ <= a ) )
assume A3: a in A ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in B & b₁ <= a )
take b = a; :: thesis: ( b in B & b <= a )
thus ( b in B & b <= a ) by A1, A3; :: thesis: verum