defpred S₁[ set ] means ex a, b, c, d being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( $1 = [a,b,c,d] & (((a `1 ) - (b `1 )) * ((c `2 ) - (d `2 ))) - (((c `1 ) - (d `1 )) * ((a `2 ) - (b `2 ))) = 0. F & (((a `1 ) - (b `1 )) * ((c `3 ) - (d `3 ))) - (((c `1 ) - (d `1 )) * ((a `3 ) - (b `3 ))) = 0. F & (((a `2 ) - (b `2 )) * ((c `3 ) - (d `3 ))) - (((c `2 ) - (d `2 )) * ((a `3 ) - (b `3 ))) = 0. F );
thus ex X being set st
for x being set holds
( x in X iff ( x in 4C3 F & S₁[x] ) ) from XBOOLE_0:sch 1(); :: thesis: verum