reconsider A = IntRel L as auxiliary Relation of ;
A is approximating by Th41;
hence ex b₁ being Relation of st
( b₁ is approximating & b₁ is auxiliary ) ; :: thesis: verum