for i, n being Nat st i in Seg n holds
( AxialSymmetry (i,n) is V254( F_Real ) & (AxialSymmetry (i,n)) ~ = AxialSymmetry (i,n) )