:: deftheorem defines 4C_3 PARSP_1:def 8 :
for F being Field holds 4C_3 F = [:[:(C_3 F),(C_3 F):],[:(C_3 F),(C_3 F):]:];