set a = the HIPERPLANE of V;

set D = { the HIPERPLANE of V};

take { the HIPERPLANE of V} ; :: thesis: for x being set st x in { the HIPERPLANE of V} holds

x is HIPERPLANE of V

thus for x being set st x in { the HIPERPLANE of V} holds

x is HIPERPLANE of V by TARSKI:def 1; :: thesis: verum

set D = { the HIPERPLANE of V};

take { the HIPERPLANE of V} ; :: thesis: for x being set st x in { the HIPERPLANE of V} holds

x is HIPERPLANE of V

thus for x being set st x in { the HIPERPLANE of V} holds

x is HIPERPLANE of V by TARSKI:def 1; :: thesis: verum