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