let A1, A2 be set ; :: thesis: ( ( for a being set holds
( a in A1 iff a is auxiliary Relation of L ) ) & ( for a being set holds
( a in A2 iff a is auxiliary Relation of L ) ) implies A1 = A2 )
assume that
A2: for a being set holds
( a in A1 iff a is auxiliary Relation of L ) and
A3: for a being set holds
( a in A2 iff a is auxiliary Relation of L ) ; :: thesis: A1 = A2
thus A1 = A2 :: thesis: verum

proof

thus A1 c= A2 :: according to XBOOLE_0:def 10 :: thesis: A2 c= A1

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A1 or a in A2 )
assume a in A1 ; :: thesis: a in A2
then a is auxiliary Relation of L by A2;
hence a in A2 by A3; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A2 or a in A1 )
assume a in A2 ; :: thesis: a in A1
then a is auxiliary Relation of L by A3;
hence a in A1 by A2; :: thesis: verum

end;