let D1, D2 be LINE_DOMAIN of V; :: thesis: ( ( for x being set holds
( x in D1 iff x is LINE of V ) ) & ( for x being set holds
( x in D2 iff x is LINE of V ) ) implies D1 = D2 )
assume that
A4: for x being set holds
( x in D1 iff x is LINE of V ) and
A5: for x being set holds
( x in D2 iff x is LINE of V ) ; :: thesis: D1 = D2

now

let x be set ; :: thesis: ( x in D1 iff x in D2 )
( x in D1 iff x is LINE of V ) by A4;
hence ( x in D1 iff x in D2 ) by A5; :: thesis: verum

end;

hence D1 = D2 by TARSKI:2; :: thesis: verum